proposition: Theorem max_l : forall n m, m <= n -> max n m = n.
proof: Proof. intros n m; revert n; simple_induction m m IHm; auto. intros [] p. 1: inversion p. cbn; by apply ap_S, IHm, leq_S_n. Defined.
imports: Basics Types Basics.Nat HoTT.DProp