proposition: Lemma mono_inj_in : {in D &, {mono f : x y / aR x y >-> rR x y}} -> {in D &, injective f}.
proof: Proof. by move=> mf x y ?? eqf; apply/aR_anti; rewrite -!mf// eqf rR_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)