n m k : nat_min n (nat_min m k) = nat_min (nat_min 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