proposition: Lemma CReal_abs_mult : forall x y : CReal, CReal_abs (x * y) == CReal_abs x * CReal_abs y.
proof: Proof. assert (forall x y : CReal, x # 0 -> y # 0 -> CReal_abs (x * y) == CReal_abs x * CReal_abs y) as prep. { intros. destruct H, H0. - rewrite CReal_abs_right, CReal_abs_left, CReal_abs_left. + ring. + apply CRealLt_asym, c0. + apply CRealLt_asym, c. + setoid_replace (x*y) with (- x * - y). * apply CRealLt_asym, CReal_mult_lt_0_compat. -- rewrite <- CReal_opp_0. apply CReal_opp_gt_lt_contravar, c. -- rewrite <- CReal_opp_0. apply CReal_opp_gt_lt_contravar, c0. * ring. - rewrite CReal_abs_left, CReal_abs_left, CReal_abs_right. + ring. + apply CRealLt_asym, c0. + apply CRealLt_asym, c. + rewrite <- (CReal_mult_0_l y). apply CReal_mult_le_compat_r. * apply CRealLt_asym, c0. * apply CRealLt_asym, c. - rewrite CReal_abs_left, CReal_abs_right, CReal_abs_left. + ring. + apply CRealLt_asym, c0. + apply CRealLt_asym, c. + rewrite <- (CReal_mult_0_r x). apply CReal_mult_le_compat_l. * apply CRealLt_asym, c. * apply CRealLt_asym, c0. - rewrite CReal_abs_right, CReal_abs_right, CReal_abs_right. + ring. + apply CRealLt_asym, c0. + apply CRealLt_asym, c. + apply CRealLt_asym, CReal_mult_lt_0_compat; assumption. } split. - intro abs. assert (0 < CReal_abs x * CReal_abs y). { apply (CReal_le_lt_trans _ (CReal_abs (x*y))). - apply CReal_abs_pos. - exact abs. } pose proof (CReal_mult_pos_appart_zero _ _ H). rewrite CReal_mult_comm in H. apply CReal_mult_pos_appart_zero in H. destruct H. 2: apply (CReal_abs_pos y c). destruct H0. 2: apply (CReal_abs_pos x c0). apply CReal_abs_appart_0 in c. apply CReal_abs_appart_0 in c0. rewrite (prep x y) in abs. + exact (CRealLt_asym _ _ abs abs). + exact c0. + exact c. - intro abs. assert (0 < CReal_abs (x * y)). { apply (CReal_le_lt_trans _ (CReal_abs x * CReal_abs y)). - rewrite <- (CReal_mult_0_l (CReal_abs y)). apply CReal_mult_le_compat_r. + apply CReal_abs_pos. + apply CReal_abs_pos. - exact abs. } apply CReal_abs_appart_0 in H. destruct H. + apply CReal_opp_gt_lt_contravar in c. rewrite CReal_opp_0, CReal_opp_mult_distr_l in c. pose proof (CReal_mult_pos_appart_zero _ _ c). rewrite CReal_mult_comm in c. apply CReal_mult_pos_appart_zero in c. rewrite (prep x y) in abs. * exact (CRealLt_asym _ _ abs abs). * destruct H. -- left. apply CReal_opp_gt_lt_contravar in c0. rewrite CReal_opp_involutive, CReal_opp_0 in c0. exact c0. -- right. apply CReal_opp_gt_lt_contravar in c0. rewrite CReal_opp_involutive, CReal_opp_0 in c0. exact c0. * destruct c. -- right. exact c. -- left. exact c. + pose proof (CReal_mult_pos_appart_zero _ _ c). rewrite CReal_mult_comm in c. apply CReal_mult_pos_appart_zero in c. rewrite (prep x y) in abs. * exact (CRealLt_asym _ _ abs abs). * destruct H. -- right. exact c0. -- left. exact c0. * destruct c. -- right. exact c. -- left. exact c. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra