proposition: Lemma cards_eqP A : cards_eq_spec A (enum A) A #|A|.
proof: Proof. by move: (enum A) (cardE A) (set_enum A) (enum_uniq A) => s -> <-; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)