proposition: Theorem min_l : forall n m : nat, n <= m -> min n m = n.
proof: Proof. simple_induction n n IHn; auto. intros [] p. 1: inversion p. cbn; by apply ap_S, IHn, leq_S_n. Defined.
imports: Basics Types Basics.Nat HoTT.DProp