proposition: Lemma SizeMonotonicOptFP_proof A (g : nat -> E (option A)) : (forall s s1 s2, (s1 <= s2)%coq_nat -> (semProdSizeOpt (g s1) s \subset semProdSizeOpt (g s2) s) /\ (~ semProdSize (g s1) s None -> semProdSize (g s1) s <--> semProdSize (g s2) s) /\ (isNone :&: semProdSize (g s2) s \subset isNone :&: semProdSize (g s1) s)) -> SizedMonotonicOptFP g.
proof: Proof. intros H. constructor. intro; intros. eapply H; eauto. intro; intros. eapply H; eauto. intro; intros. eapply H; eauto. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Enumerators Checker Decidability CheckerProofs Ltac2(Ltac2) mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq)