{n m} : n <= m -> nat_min n m = n. Proof. revert n m. simple_induction n n IHn; auto. intros [] p. 1: inversion p. cbn; by apply (ap S), IHn, leq_pred'. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids