proposition: Lemma inj_eqAxiom : injective f -> Equality.axiom (fun x y => f x == f y).
proof: Proof. by move=> f_inj x y; apply: (iffP eqP) => [|-> //]; apply: f_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)