proposition: Lemma Mengolli_Sum_gen : forall f g : nat -> G, (forall n, g n [=] f (S n) [-]f n) -> forall m n, m <= S n -> Sum m n g [=] f (S n) [-]f m.
proof: Proof. intros f g H m n; induction n as [| n Hrecn]; intro Hmn. elim (le_lt_eq_dec _ _ Hmn); intro H0. cut (m = 0); [ intro H1 | inversion H0; auto with arith; inversion H2 ]. rewrite H1. eapply eq_transitive_unfolded; [ apply Sum_one | apply H ]. cut (0 = pred 1); [ intro H1 | auto ]. rewrite H0; astepr ([0]:G); rewrite H1; apply Sum_empty. auto with arith. simpl in Hmn; elim (le_lt_eq_dec _ _ Hmn); intro H0. apply eq_transitive_unfolded with (f (S (S n)) [-]f (S n) [+] (f (S n) [-]f m)). eapply eq_transitive_unfolded. apply Sum_last. eapply eq_transitive_unfolded. apply cag_commutes_unfolded. apply bin_op_wd_unfolded; [ apply H | apply Hrecn ]. auto with arith. astepr (f (S (S n)) [+][0][-]f m). astepr (f (S (S n)) [+] ([--] (f (S n)) [+]f (S n)) [-]f m). Step_final (f (S (S n)) [+] [--] (f (S n)) [+]f (S n) [-]f m). rewrite H0. astepr ([0]:G). cut (S n = pred (S (S n))); [ intro H2 | auto ]. rewrite H2; apply Sum_empty. auto with arith. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)