proposition: Lemma Rabs_triang_inv2 : forall a b:R, Rabs (Rabs a - Rabs b) <= Rabs (a - b).
proof: Proof. cut (forall a b:R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)). - intros; destruct (Rtotal_order (Rabs a) (Rabs b)) as [Hlt| [Heq| Hgt]]. + rewrite <- (Rabs_Ropp (Rabs a - Rabs b)); rewrite <- (Rabs_Ropp (a - b)); do 2 rewrite Ropp_minus_distr. apply H; left; assumption. + rewrite Heq; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rabs_pos. + apply H; left; assumption. - intros; replace (Rabs (Rabs a - Rabs b)) with (Rabs a - Rabs b). + apply Rabs_triang_inv. + rewrite (Rabs_right (Rabs a - Rabs b)); [ reflexivity | apply Rle_ge; apply Rplus_le_reg_l with (Rabs b); rewrite Rplus_0_r; replace (Rabs b + (Rabs a - Rabs b)) with (Rabs a); [ assumption | ring ] ]. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp