proposition: Lemma homo_ltn_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) : (forall y x z, r x y -> r y z -> r x z) -> {in D &, forall i j k, i < k < j -> k \in D} -> {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} -> {in D &, {homo f : i j / i < j >-> r i j}}.
proof: Proof. move=> r_trans Dcx r_incr i j iD jD lt_ij; move: (lt_ij) (jD) => /subnKC<-. elim: (_ - _) => [|k ihk]; first by rewrite addn0 => Dsi; apply: r_incr. move=> DSiSk [: DSik]; apply: (r_trans _ _ _ (ihk _)); rewrite ?addnS. by abstract: DSik; apply: (Dcx _ _ iD DSiSk); rewrite ltn_addr ?addnS /=. by apply: r_incr; rewrite -?addnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring