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