proposition: Lemma semOptBind A B (g : G A) (f : A -> G (option B)) : SizeMonotonic g -> (forall a : A, SizeMonotonicOpt (f a)) -> semProdOpt (bind g f) <--> \bigcup_(a in semProd g) semProdOpt (f a).
proof: Proof. intros Hs Hsf. rewrite /semProdOpt /semProd. setoid_rewrite semBindSize. intro b. split. - intros [s [_ [a [H1 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 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)