proposition: Lemma Sum0_strext : forall f g n, Sum0 n f [#] Sum0 n g -> {i:nat | i < n | f i [#] g i}.
proof: Proof. intros f g n H. induction n as [| n Hrecn]. simpl in H. elim (ap_irreflexive_unfolded _ _ H). simpl in H. cut ({i : nat | i < n | f i [#] g i} or f n [#] g n). intro H0. elim H0; intro H1. elim H1; intros i H2 H3; exists i; auto with arith. exists n; auto with arith. cut (Sum0 n f [#] Sum0 n g or f n [#] g n). intro H0; elim H0; intro H1. left; apply Hrecn; assumption. auto. apply bin_op_strext_unfolded with (csg_op (c:=G)). assumption. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)