nat_max_assoc@{} n m k : nat_max n (nat_max m k) = nat_max (nat_max n m) k. Proof. induction n as [|n IHn] in m, k |- *. 1: reflexivity. destruct m, k. 1-3: reflexivity. by apply (ap S), IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids