proposition: Lemma plus_min_distr_l : forall n m p, Qcmin (p + n) (p + m) = p + Qcmin n m.
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 Qcle_refl. now apply Qclt_le_weak. repeat rewrite min_r. reflexivity. assumption. apply Qcplus_le_compat. now apply Qcle_refl. assumption. Qed.
imports: QArith_base Qcanon Orders GenericMinMax ClassicalRealizability.QcOrderedType