proposition: Lemma Rabs_triang : forall a b:R, Rabs (a + b) <= Rabs a + Rabs b.
proof: Proof. intros a b; unfold Rabs; case (Rcase_abs (a + b)) as [Hlt|Hge]; case (Rcase_abs a) as [Hlta|Hgea]; case (Rcase_abs b) as [Hltb|Hgeb]. - apply (Req_le (- (a + b)) (- a + - b)); rewrite (Ropp_plus_distr a b); reflexivity. - rewrite (Ropp_plus_distr a b); apply (Rplus_le_compat_l (- a) (- b) b); unfold Rle; elim Hgeb; intro. + left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- b) 0 b H); intro; elim (Rplus_ne (- b)); intros v w; rewrite v in H0; clear v w; rewrite (Rplus_opp_l b) in H0; apply (Rlt_trans (- b) 0 b H0 H). + right; rewrite H; apply Ropp_0. - rewrite (Ropp_plus_distr a b); rewrite (Rplus_comm (- a) (- b)); rewrite (Rplus_comm a (- b)); apply (Rplus_le_compat_l (- b) (- a) a); unfold Rle; elim Hgea; intro. + left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- a) 0 a H); intro; elim (Rplus_ne (- a)); intros v w; rewrite v in H0; clear v w; rewrite (Rplus_opp_l a) in H0; apply (Rlt_trans (- a) 0 a H0 H). + right; rewrite H; apply Ropp_0. - exfalso; generalize (Rplus_ge_compat_l a b 0 Hgeb); intro; elim (Rplus_ne a); intros v w; rewrite v in H; clear v w; generalize (Rge_trans (a + b) a 0 H Hgea); intro; clear H; unfold Rge in H0; elim H0; intro; clear H0. + unfold Rgt in H; generalize (Rlt_asym (a + b) 0 Hlt); intro; auto. + absurd (a + b = 0); auto. apply (Rlt_dichotomy_converse (a + b) 0); left; assumption. - exfalso; generalize (Rplus_lt_compat_l a b 0 Hltb); intro; elim (Rplus_ne a); intros v w; rewrite v in H; clear v w; generalize (Rlt_trans (a + b) a 0 H Hlta); intro; clear H; destruct Hge. + unfold Rgt in H; generalize (Rlt_trans (a + b) 0 (a + b) H0 H); intro; apply (Rlt_irrefl (a + b)); assumption. + rewrite H in H0; apply (Rlt_irrefl 0); assumption. - rewrite (Rplus_comm a b); rewrite (Rplus_comm (- a) b); apply (Rplus_le_compat_l b a (- a)); apply (Rminus_le a (- a)); unfold Rminus; rewrite (Ropp_involutive a); generalize (Rplus_lt_compat_l a a 0 Hlta); clear Hge Hgeb; intro; elim (Rplus_ne a); intros v w; rewrite v in H; clear v w; generalize (Rlt_trans (a + a) a 0 H Hlta); intro; apply (Rlt_le (a + a) 0 H0). - apply (Rplus_le_compat_l a b (- b)); apply (Rminus_le b (- b)); unfold Rminus; rewrite (Ropp_involutive b); generalize (Rplus_lt_compat_l b b 0 Hltb); clear Hge Hgea; intro; elim (Rplus_ne b); intros v w; rewrite v in H; clear v w; generalize (Rlt_trans (b + b) b 0 H Hltb); intro; apply (Rlt_le (b + b) 0 H0). - unfold Rle; right; reflexivity. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp