proposition: Lemma fsubEproper A B : (A `<=` B) = (A == B) || (A `<` B).
proof: Proof. by rewrite fproperEneq; case: eqP => //= ->; apply: fsubset_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)