proposition: Fact msum_ext n f g : (forall i, i < n -> f i = g i) -> ∑ n f = ∑ n g.
proof: Proof. revert f g; induction n as [ | n IHn ]; intros f g Hfg; simpl; f_equal; auto. + apply Hfg; lia. + apply IHn; intros; apply Hfg; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)