proposition: Lemma triangle_Sum : forall m n (z : nat -> CC), m <= S n -> AbsCC (Sum m n z) [<=] Sum m n (fun i => AbsCC (z i)).
proof: Proof. intros. induction n as [| n Hrecn]; intros. generalize (toCle _ _ H); clear H; intro H. inversion H as [|m0 H1 H2]. unfold Sum in |- *. unfold Sum1 in |- *. astepl (AbsCC [0]). astepr ZeroR. astepr (AbsCC [0]). apply leEq_reflexive. inversion H1. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. cut (AbsCC ([0][+]z 0[-][0])[<=][0][+]AbsCC (z 0)[-][0]). auto. apply eq_imp_leEq. rstepr (AbsCC (z 0)). apply AbsCC_wd. rational. elim (le_lt_eq_dec _ _ H); intro y. astepl (AbsCC (Sum m n z[+]z (S n))). apply leEq_wdr with (Sum m n (fun i : nat => AbsCC (z i))[+]AbsCC (z (S n))). apply leEq_transitive with (AbsCC (Sum m n z)[+]AbsCC (z (S n))). apply triangle. apply plus_resp_leEq. apply Hrecn. auto with arith. apply eq_symmetric_unfolded. apply Sum_last with (f := fun i : nat => AbsCC (z i)). rewrite y. unfold Sum in |- *. unfold Sum1 in |- *. astepl (AbsCC [0]). astepr ZeroR. astepr (AbsCC [0]). apply leEq_reflexive. Qed.
imports: CoRN.complex.CComplex