proposition: Lemma Sum_term : forall f m i n, m <= i -> i <= n -> (forall j, m <= j -> j <> i -> j <= n -> f j [=] [0]) -> Sum m n f [=] f i.
proof: Proof. intros a k i0 l H H0 H1. astepl (Sum k i0 a[+]Sum (S i0) l a). astepr (a i0[+][0]). apply bin_op_wd_unfolded. elim (O_or_S i0); intro H2. elim H2; intros m Hm. rewrite <- Hm. astepl (Sum k m a[+]a (S m)). astepr ([0][+]a (S m)). apply bin_op_wd_unfolded. apply Sum_zero. rewrite Hm; auto. intros i H3 H4. apply H1. auto. lia. lia. algebra. rewrite <- H2 in H. rewrite <- H2. inversion H. algebra. apply Sum_zero. auto with arith. intros. apply H1. lia. lia. auto. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)