proposition: Lemma extract_positive : forall {A1 A2 B1 B2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {chB1 : Choice.class_of B1} {chB2 : Choice.class_of B2} (dA : SDistr_carrier (F_choice_prod_obj ⟨ Choice.Pack chA1, Choice.Pack chA2 ⟩)) (FF1 : _ -> SDistr (F_choice_prod ⟨ Choice.Pack chB1, Choice.Pack chB2 ⟩)) b1 b2, 0 < (\dlet_(i <- dA) (FF1 i)) (b1, b2) -> exists (a1 : Choice.Pack chA1) (a2 : Choice.Pack chA2), 0 < dA (a1, a2) /\ 0 < FF1 (a1, a2) (b1, b2).
proof: Proof. intuition. rewrite /(\dlet_(i <- _) _) in H. unlock in H. simpl in H. rewrite /mlet in H. rewrite lt0r in H. move: H=> /andP [H1 H2]. move: H1 => /negP H1. have H1prop : ~ (psum (fun (x : F_choice_prod_obj ⟨ Choice.Pack chA1, Choice.Pack chA2 ⟩) => (dA x * FF1 x (b1, b2))) = 0). { move=> absrd. rewrite absrd in H1. apply H1. trivial. } apply neq0_psum in H1prop. destruct H1prop as [[a1 a2] bla]. repeat unshelve esplit. exact a1. exact a2. - destruct dA as [dAmap dAz dAsmbl dApsum]. simpl in *. rewrite lt0r. apply /andP ; split. apply /negP. move=> absrd. apply bla. move: absrd=> /eqP absrd. rewrite absrd. rewrite GRing.mul0r //=. apply dAz. - destruct (FF1 (a1,a2)) as [FF1map FF1z FF1smbl FF1psum]. simpl in *. rewrite lt0r. apply /andP ; split. apply /negP. move=> absrd. apply bla. move: absrd=> /eqP absrd. rewrite absrd. rewrite GRing.mulr0 //=. apply FF1z. Qed.
imports: mathcomp(all_ssreflect all_algebra boolp distr reals realsum) Mon(SpecificationMonads SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd SubDistr Couplings Axioms)