theorem proved term proof

`ordering_B_equal`

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

formal statement (Lean)

 102theorem ordering_B_equal : (8+11 : ℕ) = 6+13 := by omega

Term-mode proof.

 103
 104/-- Ordering A has distinct up/down spans. -/

Lean names referenced from this declaration's body.