proposition: Lemma incr_equiv r : (forall (i j : nat), i < j < (size r) -> nth Z r i <=R nth Z r j) <-> (forall (i : nat), i.+1 < (size r) -> nth Z r i <=R nth Z r i.+1).
proof: Proof. Proof using Rtrans. split => H. - by move=> i Hi; apply: H; rewrite Hi ltnSn. - move=> i j; move Hdiff : (j - i.+1) => diff. elim: diff i j Hdiff => [| diff IHdiff] i j /=. + move/eqP; rewrite -/(leq j i) => /eqP H1 /andP[H2 Hj]. have Hij : i.+1 = j by apply/eqP; rewrite eqn_leq H2 /= /leq H1. by rewrite -Hij; apply: H; rewrite Hij. + move=> Hdiff => /andP[_ Hj]. have Hij : i < j.-1. by move: Hdiff; rewrite subnS -subn1 subnAC subn1 -subn_gt0 => ->. apply: (Rtrans (y := nth Z r j.-1)). - apply: IHdiff; last by rewrite Hij /=; apply (leq_ltn_trans (leq_pred _)). apply/eqP; rewrite -eqSS -Hdiff. rewrite -(subSn Hij). by move: Hij; case j. - by case: j Hj Hij {Hdiff} => [//= | j ] /H /=. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)