proposition: Lemma pickDrop_def : forall {A} (l: list (nat * G (option A))) n, sum_fst l <= n -> pickDrop l n = (0, ret None, l).
proof: Proof. move=> A l n Hleq. elim : l n Hleq => //=. case=> //= i p l IHl n Hleq. rewrite sum_fstE in Hleq. remember (n < i). case: b Heqb => Heqb; symmetry in Heqb. - have : (i + sum_fst l) < i by eapply (leq_ltn_trans); eassumption. rewrite -ltn_subRL. by have -> : forall i, (i - i) = 0 by elim. - rewrite IHl; auto. rewrite -(leq_add2r i) subnK. by rewrite addnC. by apply/not_lt. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)