proposition: Lemma fsubset_ext : ∀ (A : ordType) (s1 s2 : {fset A}), (∀ x, x \in s1 → x \in s2) → fsubset s1 s2.
proof: Proof. intros A s1 s2 h. cbn. apply/eqP. pose proof (eq_fset (s1 :|: s2) s2) as [h1 h2]. forward h1. { intro x. rewrite in_fsetU. destruct (x \in s1) eqn:e. - cbn. symmetry. apply h. auto. - cbn. reflexivity. } rewrite h1. reflexivity. 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)