proposition: Lemma fsubset1 A x : (A `<=` [fset x]) = (A == [fset x]) || (A == fset0).
proof: Proof. rewrite eqEfcard cardfs1 -cardfs_eq0 orbC andbC. by case: posnP => // A0; rewrite (cardfs0_eq A0) fsub0set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)