proposition: Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal), r # 0 -> r * r1 == r * r2 -> r1 == r2.
proof: Proof. intros. destruct H; split. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. + rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. exact (CRealLe_refl _ abs). + apply (CReal_plus_lt_reg_l r). rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. + rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. exact (CRealLe_refl _ abs). + apply (CReal_plus_lt_reg_l r). rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. + rewrite H0 in abs. exact (CRealLe_refl _ abs). + exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. + rewrite H0 in abs. exact (CRealLe_refl _ abs). + exact c. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra