proposition: Lemma plus_min_distr_r : forall n m p, Qcmin (n + p) (m + p) = Qcmin n m + p.
proof: Proof. intros n m p. destruct (Qclt_le_dec n m). repeat rewrite min_l. reflexivity. now apply Qclt_le_weak. apply Qcplus_le_compat. now apply Qclt_le_weak. now apply Qcle_refl. repeat rewrite min_r. reflexivity. assumption. apply Qcplus_le_compat. assumption. now apply Qcle_refl. Qed.
imports: QArith_base Qcanon Orders GenericMinMax ClassicalRealizability.QcOrderedType