proposition: Lemma pickDrop_In : forall {A} (l: list (nat * G (option A))) k x, List.In (k,x) l /\ k <> 0 -> exists n l', pickDrop l n = (k,x,l').
proof: Proof. move => A l k x [HIn Hfst]. elim : l HIn => //=. case => //= i g xs IHxs [H1 | H2]; subst. + exists 0. exists xs. simpl in *. inversion H1; subst; clear H1. have H : 0 < k by elim : k Hfst IHxs => //=. rewrite H. by split => //=. + move/(_ H2) : IHxs => [n [l' Hpick]]. exists (n + i). exists ((i,g)::l'). rewrite -[X in _ < X]add0n ltn_add2r ltn0. rewrite -[X in _ - X]add0n subnDr subn0. by rewrite Hpick. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)