proposition: Lemma Sum_zero : forall f m n, m <= S n -> (forall i, m <= i -> i <= n -> f i [=] [0]) -> Sum m n f [=] [0].
proof: Proof. intros a k l H H0. induction l as [| l Hrecl]. elim (le_lt_eq_dec _ _ H); clear H; intro H. replace k with 0. astepl (a 0). apply H0. auto. auto with arith. auto. inversion H. auto. inversion H2. rewrite H. unfold Sum in |- *. unfold Sum1 in |- *. algebra. elim (le_lt_eq_dec k (S (S l)) H); intro HH. astepl (Sum k l a[+]a (S l)). astepr ([0][+] ([0]:G)). apply bin_op_wd_unfolded. apply Hrecl; auto with arith. apply H0; auto with arith. rewrite HH. unfold Sum in |- *. unfold Sum1 in |- *. algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)