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