proposition: Lemma inj_card_onto y : y \in codom f.
proof: Proof. by move: y; apply/subset_cardP; rewrite ?card_codom ?subset_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)