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