theorem
other
other
ordering_A_unequal
show as:
view Lean formalization →
formal statement (Lean)
101theorem ordering_A_unequal : (13+11 : ℕ) ≠ 6+8 := by omega