proposition: Lemma bij_card_eq (A B: finType) (f : A -> B) : bijective f -> #|A| = #|B|.
proof: Proof. case => g can_f can_g. apply/eqP. rewrite eqn_leq (inj_card_leq (f := f)) ?(inj_card_leq (f := g)) //; exact: can_inj. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)