proposition: Lemma tuto_eq_card : forall A B, A =i B -> #|A| = #|B|.
proof: Proof. by move=> A B eqAB; rewrite !cardE (eq_enum eqAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)