proposition: Lemma multiTriangleIneg : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n : nat), CRabs R (CRsum u n) <= CRsum (fun k => CRabs R (u k)) n.
proof: Proof. induction n. - apply CRle_refl. - simpl. apply (CRle_trans _ (CRabs R (CRsum u n) + CRabs R (u (S n)))). + apply CRabs_triang. + apply CRplus_le_compat. * apply IHn. * apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits