proposition: Lemma Sum_apzero : forall f m n, m <= n -> Sum m n f [#] [0] -> {i : nat | m <= i /\ i <= n | f i [#] [0]}.
proof: Proof. intros a k l H H0. induction l as [| l Hrecl]. exists 0. split; auto. cut (k = 0). intro H'. rewrite H' in H0. astepl (Sum 0 0 a). auto. inversion H. auto. elim (le_lt_eq_dec k (S l) H); intro HH. cut (Sum k l a [#] [0] or a (S l) [#] [0]). intro H1. elim H1; clear H1; intro H1. elim Hrecl; auto with arith. intro i. intros H2 H6. exists i; auto. elim H2; intros H3 H4; auto. exists (S l); try split; auto with arith. apply cg_add_ap_zero. apply ap_wdl_unfolded with (Sum k (S l) a). auto. apply Sum_last. rewrite HH in H0. exists (S l); auto. astepl (Sum (S l) (S l) a). auto. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)