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