proposition: Lemma Rmult_1_l : forall r:R, 1 * r = r.
proof: Proof. intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1. apply CReal_mult_1_l. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions