fact: Definition vectorOf {A : Type} (k : nat) (g : G A) : G (list A) := foldr (fun m m' => bind m (fun x => bind m' (fun xs => ret (cons x xs))) ) (ret nil) (nseq k g).
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)