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