fact: Fixpoint pickDrop {A : Type} (xs : list (nat * G (option A))) n : nat * G (option A) * list (nat * G (option A)) := match xs with | nil => (0, ret None, nil) | (k, x) :: xs => if (n < k) then (k, x, xs) else let '(k', x', xs') := pickDrop xs (n - k) in (k', x', (k,x)::xs') end.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)