proposition: Lemma inj_in_eq : {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}.
proof: Proof. by move=> inj_f x y Dx Dy; apply/eqP/eqP=> [|-> //]; apply: inj_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)