Theorem: Nat.or_eq (Logic/Vorspiel/Arith.lean)

State before:
n m : ℕ
⊢ n.or m = if 0 < n ∨ 0 < m then 1 else 0
Tactic:
simp[or, isLtNat]
State after:
no goals