proposition: Lemma minus_min_distr_l : forall n m p, Rmin (p - n) (p - m) = p - Rmax n m.
proof: Proof. unfold Rminus. intros. rewrite opp_max_distr. apply plus_min_distr_l. Qed.
imports: Orders Rbase Rbasic_fun ROrderedType GenericMinMax