proposition: Lemma sum_fstE A x (a : A) l: sum_fst ((x, a) :: l) = x + sum_fst l.
proof: Proof. rewrite /sum_fst /=. elim: l 0 x => [n x|[n1 x1] l IHl p q] /=; first by rewrite addnC. by rewrite -IHl; congr foldl; rewrite addnAC. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)