proposition: Lemma CReal_mult_proper_0_l : forall x y : CReal, y == 0 -> x * y == 0.
proof: Proof. intros x y Hyeq0. apply CRealEq_diff; intros n. unfold CReal_mult, CReal_mult_seq, inject_Q; do 2 rewrite CReal_red_seq. simplify_Qabs. rewrite CRealEq_diff in Hyeq0. unfold inject_Q in Hyeq0; rewrite CReal_red_seq in Hyeq0. specialize (Hyeq0 (n - scale x - 1)%Z). simplify_Qabs_in Hyeq0. rewrite Qpower_minus_pos in Hyeq0 by lra; simplify_Qle_in Hyeq0. pose proof bound x (n - scale y - 1)%Z as Hxbnd. apply Weaken_Qle_QpowerFac; [lra|]. replace n with ((scale x) + (n - scale x))%Z at 3 by ring. rewrite Qpower_plus by lra. rewrite Qabs_Qmult. apply Qmult_le_compat_nonneg; (pose_Qabs_pos; lra). Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra