proposition: Lemma cardinal_small_set x: small_set x -> cardinal x <=c \1c.
proof: Proof. case /small_set_pr. by move ->; rewrite cardinal_set0; fprops. move =>[v ->]; rewrite cardinal_set1; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)