proposition: Lemma pick_exists : forall {A} (l: list (nat * G A)) n def, n < sum_fst l <-> exists x, List.In x l /\ pick def l n = x /\ fst x <> 0.
proof: Proof. move => A l n def. split. - move => Hlt. elim : l n Hlt => //. case => i p xs IHxs n Hlt. rewrite sum_fstE in Hlt. move/(_ (n-i)) : IHxs => IHxs. simpl. remember (n < i). case: b Heqb => [Heqb | /not_lt Heqb]. + exists (i, p). split => //=. by left. split => //=. move => contra; subst. by rewrite ltn0 in Heqb. + rewrite -(ltn_add2r i) [X in _ < X]addnC subnK // in IHxs. move/(_ Hlt) : IHxs => [x [H1 [H2 H3]]]. by exists x; split; [right | split]. - move => [x [HIn [Hpick Hneq]]]. remember (n < sum_fst l). case: b Heqb => //= /not_lt/pick_def H. rewrite H in Hpick. rewrite -Hpick //= in Hneq. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)