proposition: Lemma CReal_mult_pos_appart_zero : forall x y : CReal, 0 < x * y -> 0 # x.
proof: Proof. intros x y H0ltxy. unfold CRealLt, CReal_mult, CReal_mult_seq, CReal_mult_scale in H0ltxy; rewrite CReal_red_seq in H0ltxy. destruct H0ltxy as [n nmaj]. cbn in nmaj; setoid_rewrite Qplus_0_r in nmaj. destruct (Q_dec 0 (seq y (n - scale x - 1)))%Q as [[H0lty|Hylt0]|Hyeq0]. - apply (Qmult_lt_compat_r _ _ (/(seq y (n - scale x - 1)))%Q ) in nmaj. 2: apply Qinv_lt_0_compat, H0lty. setoid_rewrite <- Qmult_assoc in nmaj at 2. setoid_rewrite Qmult_inv_r in nmaj. 2: lra. setoid_rewrite Qmult_1_r in nmaj. pose proof bound y (n - scale x - 1)%Z as Hybnd. apply Qabs_Qlt_condition, proj2 in Hybnd. apply Qinv_lt_contravar in Hybnd. 3: apply Qpower_0_lt; lra. 2: exact H0lty. apply (Qmult_lt_l _ _ (2 * (2 ^ n))) in Hybnd. 2: pose proof Qpower_0_lt 2 n; lra. apply (Qlt_trans _ _ _ Hybnd) in nmaj; clear Hybnd. rewrite <- Qpower_opp, <- Qmult_assoc, <- Qpower_plus in nmaj by lra. apply (CReal_abs_appart_zero x (n - scale y - 1)%Z), Qabs_gt. rewrite Qpower_minus_pos. ring_simplify. ring_simplify (n + - scale y)%Z in nmaj. pose proof Qpower_0_lt 2 (n - scale y)%Z; lra. - assert (forall a b : Q, ((-a)*(-b)==a*b)%Q) by (intros; ring). setoid_rewrite <- H in nmaj at 2; clear H. apply (Qmult_lt_compat_r _ _ (/-(seq y (n - scale x - 1)))%Q ) in nmaj. 2: apply Qinv_lt_0_compat; lra. setoid_rewrite <- Qmult_assoc in nmaj at 2. setoid_rewrite Qmult_inv_r in nmaj. 2: lra. setoid_rewrite Qmult_1_r in nmaj. pose proof bound y (n - scale x - 1)%Z as Hybnd. apply Qabs_Qlt_condition, proj1 in Hybnd. apply Qopp_lt_compat in Hybnd; rewrite Qopp_involutive in Hybnd. apply Qinv_lt_contravar in Hybnd. 3: apply Qpower_0_lt; lra. 2: lra. apply (Qmult_lt_l _ _ (2 * (2 ^ n))) in Hybnd. 2: pose proof Qpower_0_lt 2 n; lra. apply (Qlt_trans _ _ _ Hybnd) in nmaj; clear Hybnd. rewrite <- Qpower_opp, <- Qmult_assoc, <- Qpower_plus in nmaj by lra. apply (CReal_abs_appart_zero x (n - scale y - 1)%Z). pose proof Qpower_0_lt 2 (n + - scale y)%Z ltac:(lra) as Hpowpos. rewrite Qabs_neg by lra. rewrite Qpower_minus_pos. ring_simplify. ring_simplify (n + - scale y)%Z in nmaj. pose proof Qpower_0_lt 2 (n - scale y)%Z; lra. - pose proof Qpower_0_lt 2 n ltac:(lra). rewrite <- Hyeq0 in nmaj. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra