proposition: Lemma Sum_wd' : forall m n, m <= S n -> forall f f', (forall i, m <= i -> i <= n -> f i [=] f' i) -> Sum m n f [=] Sum m n f'.
proof: Proof. intros m n. induction n as [| n Hrecn]; intros H f f' H0. inversion H. unfold Sum in |- *. unfold Sum1 in |- *. Step_final ([0]:G). inversion H2. astepl (f 0). astepr (f' 0). auto. elim (le_lt_eq_dec m (S (S n)) H); intro H1. astepl (Sum m n f[+]f (S n)). astepr (Sum m n f'[+]f' (S n)). apply bin_op_wd_unfolded; auto with arith. rewrite H1. unfold Sum in |- *. unfold Sum1 in |- *. Step_final ([0]:G). Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)