proposition: Lemma injective_card A B (e : {fhrel A & B}) : is_injective e -> #|e| <= #|B|.
proof: Proof. move/fhrel_injective => inj_e. rewrite -(card_in_imset (f := @snd A B)) ?max_card //. move => [x y] [x' y']. rewrite !inE /= => E1 E2 ?; subst. by rewrite (inj_e _ _ _ E1 E2). Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)