proposition: Lemma pickDrop_exists : forall {A} (l: list (nat * G (option A))) n, n < sum_fst l <-> exists k g l', List.In (k,g) l /\ pickDrop l n = (k,g,l') /\ k <> 0 /\ l <--> [set (k, g)] :|: l' /\ length l' + 1 = length l /\ sum_fst l' + k = sum_fst l.
proof: Proof. move => A l n. 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. exists p. exists xs. split => //=. by left. split => //=. split. move => contra; subst. by rewrite ltn0 in Heqb. split. by rewrite cons_set_eq. split. by ssromega. rewrite sum_fstE. by ssromega. + rewrite -(ltn_add2r i) [X in _ < X]addnC subnK // in IHxs. move/(_ Hlt) : IHxs => [k [g [gs [H1 [H2 [H3 [H4 [H5 H6]]]]]]]]. exists k. exists g. exists ((i,p)::gs). split; [right | split; [| split; [| split; [| split]]]]; try (simpl; eauto; by rewrite H2). rewrite !cons_set_eq H4. rewrite setU_assoc (setU_comm [set (i, p)]) -setU_assoc. reflexivity. simpl. by ssromega. simpl. rewrite !sum_fstE. by ssromega. - move => [k [g [gs [HIn [Hpick [Hneq _]]]]]]. remember (n < sum_fst l). case: b Heqb => //= /not_lt/pickDrop_def H. rewrite H in Hpick. inversion Hpick; subst; eauto. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)