proposition: Lemma min_l n m : n <= m -> Nat.min n m = n.
proof: Proof. revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial. - inversion 1. - intros. apply f_equal, IHn, le_S_n; trivial. Qed.
imports: Notations Ltac Datatypes Logic