proposition: Lemma Rabs_4 : forall a b c d:R, Rabs (a + b + c + d) <= Rabs a + Rabs b + Rabs c + Rabs d.
proof: Proof. intros. apply Rle_trans with (Rabs (a + b) + Rabs (c + d)). - replace (a + b + c + d) with (a + b + (c + d)); [ apply Rabs_triang | ring ]. - apply Rle_trans with (Rabs a + Rabs b + Rabs (c + d)). + apply Rplus_le_compat_r. apply Rabs_triang. + repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l. apply Rabs_triang. Qed.
imports: Rbase Rfunctions Ranalysis1 Lra