proposition: Lemma Sum0_strext' : forall f g n, Sum0 n f [#] Sum0 n g -> {i : nat | f i [#] g i}.
proof: Proof. intros f g n H. elim (Sum0_strext _ _ _ H); intros i Hi Hi'; exists i; auto. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)