proposition: Lemma CR_double : forall {R : ConstructiveReals} (x:CRcarrier R), CR_of_Q R 2 * x == x + x.
proof: Proof. intros R x. rewrite (CR_of_Q_morph R 2 (1+1)). 2: reflexivity. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum