proposition: Lemma CReal_mult_1_l : forall r: CReal, 1 * r == r.
proof: Proof. intros r; apply CRealEq_diff; intros n. unfold inject_Q, CReal_mult, CReal_mult_seq, CReal_mult_scale. do 2 rewrite CReal_red_seq. do 1 rewrite CReal_red_scale. change (Qbound_ltabs_ZExp2 1)%Z with 1%Z. do 1 simplify_seq_idx. simplify_Qabs. pose proof cauchy r n (n-2)%Z n ltac:(lia) ltac:(lia) as Hrbnd. apply Qabs_Qlt_condition in Hrbnd. apply Qabs_Qle_condition. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra