proposition: Lemma min_r n m : m <= n -> Nat.min n m = m.
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