proposition: Lemma CReal_mult_lt_0_compat_correct : forall (x y : CReal) (Hx : 0 < x) (Hy : 0 < y), (2 * 2^(proj1_sig Hx + proj1_sig Hy - 1)%Z < seq (x * y)%CReal (proj1_sig Hx + proj1_sig Hy - 1)%Z - seq (inject_Q 0) (proj1_sig Hx + proj1_sig Hy - 1)%Z)%Q.
proof: Proof. intros x y Hx Hy. destruct Hx as [nx Hx], Hy as [ny Hy]; unfold proj1_sig. unfold inject_Q, Qminus in Hx. rewrite CReal_red_seq, Qplus_0_r in Hx. unfold inject_Q, Qminus in Hy. rewrite CReal_red_seq, Qplus_0_r in Hy. unfold CReal_mult, CReal_mult_seq, inject_Q; do 2 rewrite CReal_red_seq. rewrite Qpower_minus_pos by lra. rewrite Qpower_plus by lra. simplify_Qlt. do 2 simplify_seq_idx. apply Qmult_lt_compat_nonneg. - split. + pose proof Qpower_0_lt 2 nx; lra. + pose proof CReal_scale_sep0_limit y ny Hy as Hlimy. pose proof cauchy x nx nx (nx + ny - scale y - 2)%Z ltac:(lia) ltac:(lia) as Hbndx. apply Qabs_Qlt_condition in Hbndx. lra. - split. + pose proof Qpower_0_lt 2 ny; lra. + pose proof CReal_scale_sep0_limit x nx Hx as Hlimx. pose proof cauchy y ny ny (nx + ny - scale x - 2)%Z ltac:(lia) ltac:(lia) as Hbndy. apply Qabs_Qlt_condition in Hbndy. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra