proposition: Lemma card_size s : #|s| <= size s.
proof: Proof. elim: s => [|x s IHs] /=; first by rewrite card0. by rewrite cardU1 /=; case: (~~ _) => //; apply: leqW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)