proposition: Lemma Kneser_2a : forall (m n i : nat) (f : nat -> R), 1 <= i -> Sum m n f [=] f m[+]f i[+] (Sum (S m) (pred i) f[+]Sum (S i) n f).
proof: Proof. intros. astepl (f m[+]Sum (S m) n0 f). astepl (f m[+] (Sum (S m) i f[+]Sum (S i) n0 f)). astepl (f m[+] (Sum (S m) (pred i) f[+]f i[+]Sum (S i) n0 f)). ring. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma