fact: Fixpoint foldProd {A B : Type} (f : A -> B -> G A) (l : list B) (a : A) : G A := nosimpl( match l with | nil => ret a | (x :: xs) => bind (f a x) (foldProd f xs) end).
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)