proposition: Lemma plus_max_distr_r : forall n m p, Rmax (n + p) (m + p) = Rmax n m + p.
proof: Proof. intros. rewrite (Rplus_comm n p), (Rplus_comm m p), (Rplus_comm _ p). apply plus_max_distr_l. Qed.
imports: Orders Rbase Rbasic_fun ROrderedType GenericMinMax