proposition: Lemma plus_IQR : forall q r : Q, IQR (q + r) = IQR q + IQR r.
proof: Proof. intros. unfold IQR. apply Rquot1. rewrite Rquot2, Rrepr_plus, Rquot2, Rquot2. apply inject_Q_plus. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms