proposition: Lemma Sum_wd : forall m n f f', (forall i, f i [=] f' i) -> Sum m n f [=] Sum m n f'.
proof: Proof. intros m n f f' H. unfold Sum in |- *. unfold Sum1 in |- *. unfold cg_minus in |- *. apply bin_op_wd_unfolded. apply Sum0_wd; exact H. apply un_op_wd_unfolded. apply Sum0_wd; exact H. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)