proposition: Lemma plus_min_distr_l : forall n m p, Qmin (p + n) (p + m) == p + Qmin n m.
proof: Proof. intros. apply min_monotone. - intros x x' Hx; rewrite Hx; auto with qarith. - intros x x' Hx. apply Qplus_le_compat; q_order. Qed.
imports: QArith_base Orders QOrderedType GenericMinMax