proposition: Lemma le_nat_max_l n m : n <= Nat.Core.max n m.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness