proposition: Lemma plus_max_distr_r : forall n m p, Qmax (n + p) (m + p) == Qmax n m + p.
proof: Proof. intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p). apply plus_max_distr_l. Qed.
imports: QArith_base Orders QOrderedType GenericMinMax