proposition: Lemma sum_fst_eq0P {A} (l : list (nat * A)) : sum_fst l = 0 <-> [seq x <- l | x.1 != 0] = [::].
proof: Proof. by elim: l => [|[[|n] x] l IHl] //=; split=> //; rewrite sum_fstE. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)