proposition: Lemma plus_min_distr_l : forall n m p, Rmin (p + n) (p + m) = p + Rmin n m.
proof: Proof. intros. apply min_monotone. intros x y. apply Rplus_le_compat_l. Qed.
imports: Orders Rbase Rbasic_fun ROrderedType GenericMinMax