proposition: Lemma total_homo_mono_in : total aR -> {in D &, {homo f : x y / aR' x y >-> rR' x y}} -> {in D &, {mono f : x y / aR x y >-> rR x y}}.
proof: Proof. move=> aR_tot mf x y xD yD. have [->|neq_xy] := eqVneq x y; first by rewrite ?eqxx ?aR_refl ?rR_refl. have [xy|] := (boolP (aR x y)); first by rewrite rRE mf ?orbT// aR'E neq_xy. have /orP [->//|] := aR_tot x y. rewrite aRE eq_sym (negPf neq_xy) /= => /mf -/(_ yD xD). rewrite rR'E => /andP[Nfxfy fyfx] _; apply: contra_neqF Nfxfy => fxfy. by apply/rR_anti; rewrite fyfx fxfy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)