proposition: Lemma sum_resp_AbsSmall : forall (x y : nat -> R) (n m: nat) (H1 : m <= n) (H2 : forall i : nat, m <= i -> i <= n -> AbsSmall (y i) (x i)), AbsSmall (Sum m n y) (Sum m n x).
proof: Proof. unfold AbsSmall. intros. assert (H3 : forall i : nat, m <= i -> i <= n -> [--](y i)[<=]x i). intros. elim (H2 i H H0). auto. assert (H4 : forall i : nat, m <= i -> i <= n -> x i[<=]y i). intros. elim (H2 i H H0). auto. split. astepl (Sum m n (fun k: nat => [--](y k))). apply Sum_resp_leEq . auto with arith. intros. auto. apply Sum_resp_leEq . auto with arith. intros. auto. Qed.
imports: CoRN.algebra.COrdFields2