proposition: Lemma semSized_opt A (f : nat -> G (option A)) `{H : forall n, SizeMonotonicOpt (f n)} `{H' : @SizedMonotonicOpt _ _ PG f} : isSome :&: semProd (sized f) <--> isSome :&: \bigcup_n (semProd (f n)).
proof: Proof. rewrite semSized. rewrite !setI_bigcup_assoc. move => x; split. - move => [n [HT [Hs1 Hs2]]]. eexists. split; eauto. split; eauto. eexists; eauto. - move => [n [HT [Hs1 [m [HT' Hs2]]]]]. eexists (m + n). split. now constructor. split; [ eassumption | ]. destruct x as [ x | ]. + eapply monotonicOpt with (s2 := m + n) in Hs2; [| now ssromega ]. eapply sizeMonotonicOpt with (s1 := n) (s2 := m + n); [now ssromega |]. auto. + inv Hs1. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)