proposition: Lemma homo_leq (f : nat -> T) (r : T -> T -> Prop) : (forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) -> (forall i, r (f i) (f i.+1)) -> {homo f : i j / i <= j >-> r i j}.
proof: Proof. by move=> rrefl /(@homo_leq_in predT f r) fr fS i j; apply: fr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring