proposition: Lemma semBindSizeMonotonic {A B} (g : G A) (f : A -> G B) `{Hg : @SizeMonotonic _ _ PG g} `{Hf : forall a, SizeMonotonic (f a)} : semProd (bind g f) <--> \bigcup_(a in semProd g) semProd (f a).
proof: Proof. rewrite /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 Hg; last eassumption. lia. eapply Hf; last eassumption. lia. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)