exact if c: a ≤ b
then by
  unfold max
  unfold Nat.instMaxNat
  unfold maxOfLe 
  simp [if_pos c]
else by 
  unfold max
  unfold Nat.instMaxNat
  unfold maxOfLe
  simp [if_neg c]
  apply Nat.le_of_lt
  let c' := Nat.gt_of_not_le c
  assumption
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
⊢ b ≤ max a b
no goals