Theorem: Mt.Utils.Nat.zero_max (Mt/Utils/Nat.lean)

State before:
⊢ ∀ (a : Nat), Nat.max 0 a = a
Tactic:
intro a
State after:
a : Nat
⊢ Nat.max 0 a = a

State before:
a : Nat
⊢ Nat.max 0 a = a
Tactic:
simp only [Nat.max, Nat.zero_le, ite_true]
State after:
a : Nat
⊢ max 0 a = a