nat_max_l@{} {n m} : m <= n -> nat_max n m = n. Proof. intros H. induction m as [|m IHm] in n, H |- *. 1: nrapply nat_max_zero_r. destruct n. 1: inversion H. cbn; by apply (ap S), IHm, leq_pred'. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids