n m : nat_min n m = nat_min m n. Proof. induction n as [|n IHn] in m |- *; destruct m; cbn. 1-3: reflexivity. exact (ap S (IHn _)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids