Theorem: Nat.isEven_or_isOdd (GMLInit/Data/Nat/Coding/Sum.lean)

State before:
n : Nat
⊢ n.isEven = true ∨ n.isOdd = true
Tactic:
rw [←Bool.or_eq_true]
State after:
n : Nat
⊢ (n.isEven || n.isOdd) = true

State before:
n : Nat
⊢ (n.isEven || n.isOdd) = true
Tactic:
exact Bool.or_not_self ..
State after:
no goals