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