proposition: Lemma semBindSizeMonotonicIncl_r {A B} (g : G A) (f : A -> G (option B)) (s1 : set A) (s2 : A -> set B) : semProd g \subset s1 -> (forall x, semProd (f x) \subset Some @: (s2 x) :|: [set None]) -> semProd (bind g f) \subset Some @: (\bigcup_(a in s1) s2 a) :|: [set None].
proof: Proof. move => H1 H2 [x |] [s [_ /semBindSize [r [Hg Hf]]]]. - left. eexists; split. exists r; split; eauto. + apply H1. exists s; split; rewrite /setT; auto. + destruct (H2 r (Some x)). rewrite /semProd /setT. exists s; split; auto. * move : H => [b [Hb Heq]]. inversion Heq; subst; clear Heq. eauto. * inversion H. + unfold set1; auto. - right; reflexivity. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)