proposition: Lemma CRabs_mult : forall {R : ConstructiveReals} (x y : CRcarrier R), CRabs R (x * y) == CRabs R x * CRabs R y.
proof: Proof. intro R. assert (forall (x y : CRcarrier R), x ≶ 0 -> y ≶ 0 -> CRabs R (x * y) == CRabs R x * CRabs R y) as prep. { intros. destruct H, H0. - rewrite CRabs_right, CRabs_left, CRabs_left. + rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r, CRopp_involutive. reflexivity. + apply CRlt_asym, c0. + apply CRlt_asym, c. + setoid_replace (x*y) with (- x * - y). * apply CRlt_asym, CRmult_lt_0_compat. -- rewrite <- CRopp_0. apply CRopp_gt_lt_contravar, c. -- rewrite <- CRopp_0. apply CRopp_gt_lt_contravar, c0. * rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r, CRopp_involutive. reflexivity. - rewrite CRabs_left, CRabs_left, CRabs_right. + rewrite <- CRopp_mult_distr_l. reflexivity. + apply CRlt_asym, c0. + apply CRlt_asym, c. + rewrite <- (CRmult_0_l y). apply CRmult_le_compat_r_half. * exact c0. * apply CRlt_asym, c. - rewrite CRabs_left, CRabs_right, CRabs_left. + rewrite <- CRopp_mult_distr_r. reflexivity. + apply CRlt_asym, c0. + apply CRlt_asym, c. + rewrite <- (CRmult_0_r x). apply CRmult_le_compat_l_half. * exact c. * apply CRlt_asym, c0. - rewrite CRabs_right, CRabs_right, CRabs_right. + reflexivity. + apply CRlt_asym, c0. + apply CRlt_asym, c. + apply CRlt_asym, CRmult_lt_0_compat; assumption. } split. - intro abs. assert (0 < CRabs R x * CRabs R y). { apply (CRle_lt_trans _ (CRabs R (x*y))). - apply CRabs_pos. - exact abs. } pose proof (CRmult_pos_appart_zero _ _ H). rewrite CRmult_comm in H. apply CRmult_pos_appart_zero in H. destruct H. 2: apply (CRabs_pos y c). destruct H0. 2: apply (CRabs_pos x c0). apply CRabs_appart_0 in c. apply CRabs_appart_0 in c0. rewrite (prep x y) in abs. + exact (CRlt_asym _ _ abs abs). + exact c0. + exact c. - intro abs. assert (0 < CRabs R (x * y)). { apply (CRle_lt_trans _ (CRabs R x * CRabs R y)). - rewrite <- (CRmult_0_l (CRabs R y)). apply CRmult_le_compat_r. + apply CRabs_pos. + apply CRabs_pos. - exact abs. } apply CRabs_appart_0 in H. destruct H. + apply CRopp_gt_lt_contravar in c. rewrite CRopp_0, CRopp_mult_distr_l in c. pose proof (CRmult_pos_appart_zero _ _ c). rewrite CRmult_comm in c. apply CRmult_pos_appart_zero in c. rewrite (prep x y) in abs. * exact (CRlt_asym _ _ abs abs). * destruct H. -- left. apply CRopp_gt_lt_contravar in c0. rewrite CRopp_involutive, CRopp_0 in c0. exact c0. -- right. apply CRopp_gt_lt_contravar in c0. rewrite CRopp_involutive, CRopp_0 in c0. exact c0. * destruct c. -- right. exact c. -- left. exact c. + pose proof (CRmult_pos_appart_zero _ _ c). rewrite CRmult_comm in c. apply CRmult_pos_appart_zero in c. rewrite (prep x y) in abs. * exact (CRlt_asym _ _ abs abs). * destruct H. -- right. exact c0. -- left. exact c0. * destruct c. -- right. exact c. -- left. exact c. Qed.
imports: QArith Qabs ConstructiveReals