proposition: Lemma str_Mengolli_Sum_gen : forall (f g : nat -> G) m n, m <= S n -> (forall i, m <= i -> i <= n -> g i [=] f (S i) [-]f i) -> Sum m n g [=] f (S n) [-]f m.
proof: Proof. intros f g m n H H0. apply eq_transitive_unfolded with (Sum m n (fun i : nat => f (S i) [-]f i)). apply Sum_wd'; assumption. apply Mengolli_Sum_gen; [ intro; algebra | assumption ]. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)