n m : m <= Nat.Core.nat_max n m. Proof. revert m. induction n as [|n' IHn]; intros m; induction m as [|m' IHm]; try reflexivity; cbn. - apply zero_least. - apply le_S_S. exact (IHn m'). Qed.
Require Import