proposition: Lemma homo_mono : {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} -> {mono g : x y / rR x y >-> aR x y}.
proof: Proof. move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|]. by apply: contraNF=> /mf; rewrite !fgK. Qed.
imports: ssreflect ssrfun