proposition: Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
proof: Proof. intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions