proposition: Lemma disjoint_in_both : ∀ {T : ordType} (s1 s2 : {fset T}), fdisjoint s1 s2 → ∀ x, x \in s1 → x \in s2 → False.
proof: Proof. intros T s1 s2 hd x h1 h2. assert (x \notin s2) as h. { move: hd => /fdisjointP hd. apply hd. assumption. } rewrite h2 in h. discriminate. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)