theorem proved term proof

`ordering_A_distinct_ends`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 105theorem ordering_A_distinct_ends :
 106    ordering_A_spans.1 ≠ ordering_A_spans.2.2 := by native_decide

Term-mode proof.

 107
 108/-- Ordering B has equal up/down spans. -/

Lean names referenced from this declaration's body.