proposition: Lemma Sum_strext : forall f g m n, m <= S n -> Sum m n f [#] Sum m n g -> {i : nat | m <= i /\ i <= n | f i [#] g i}.
proof: Proof. intros f g m n H H0. induction n as [| n Hrecn]. elim (le_lt_eq_dec _ _ H); intro H2. cut (m = 0). intro H1. rewrite H1; exists 0; auto. rewrite H1 in H0. astepl (Sum 0 0 f); astepr (Sum 0 0 g); assumption. inversion H2; [ auto | inversion H3 ]. exfalso. cut (0 = pred 1); [ intro H3 | auto ]. rewrite H3 in H0. rewrite H2 in H0. apply (ap_irreflexive_unfolded G [0]). eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply H0. apply Sum_empty; auto. apply Sum_empty; auto. elim (le_lt_eq_dec _ _ H); intro Hmn. cut (Sum m n f [#] Sum m n g or f (S n) [#] g (S n)). intro H1; elim H1; intro H2. cut {i : nat | m <= i /\ i <= n | f i [#] g i}. intro H3; elim H3; intros i H4 H5; elim H4; intros H6 H7; clear H1 H4. exists i; try split; auto with arith. apply Hrecn; auto with arith. exists (S n); try split; auto with arith. apply bin_op_strext_unfolded with (csg_op (c:=G)). astepl (Sum m (S n) f); astepr (Sum m (S n) g); assumption. clear Hrecn. exfalso. cut (S n = pred (S (S n))); [ intro H1 | auto ]. rewrite H1 in H0. rewrite Hmn in H0. apply (ap_irreflexive_unfolded G [0]). eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply H0. apply Sum_empty; auto with arith. apply Sum_empty; auto with arith. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)