proposition: Lemma semOptBindOpt A B (g : G (option A)) (f : A -> G (option B)) : SizeMonotonicOpt g -> (forall a : A, SizeMonotonicOpt (f a)) -> semProdOpt (bindOpt g f) <--> \bigcup_(a in semProdOpt g) semProdOpt (f a).
proof: Proof. intros Hs Hsf. rewrite /semProdOpt /semProd /bindOpt. setoid_rewrite semBindSize. intro b. split. - intros [s [_ [a [H1 H2]]]]. destruct a. 2:{ eapply semReturnSize in H2. inv H2. } exists a. split; exists s; (split; first (compute; by []); first by[]). - intros [a [[s1 [_ H1]] [s2 [_ H2]]]]. exists (max s1 s2). split; first (compute; by []). exists (Some a). split. eapply Hs; last eassumption. lia. eapply Hsf; last eassumption. lia. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)