proposition: Lemma surjective_card A B (e : {fhrel A & B}) : is_surjective e -> #|B| <= #|e|.
proof: Proof. move/fhrel_surjective => E. pose f y := (xchoose (E y),y). have inj_f : injective f by move => x y []. rewrite -(card_codom inj_f). apply: subset_leq_card. apply/subsetP => [[x y]] /codomP => [[y'] [-> <-]]. rewrite inE /=. exact: (xchooseP (E y)). Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)