proposition: Lemma inj_homo : injective f -> {homo f : x y / aR x y >-> rR x y} -> {homo f : x y / aR' x y >-> rR' x y}.
proof: Proof. by move=> fI mf ???; apply: (@inj_homo_in D D) => //????; [apply: fI|apply: mf]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)