proposition: Lemma non_decr_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 Rrefl Rtrans. split => H. - move=> i Hi. have : i <= i.+1 < size r by rewrite Hi andbT. exact: H. - move=> i j; move Hdiff : (j - i) => diff. elim: diff i j Hdiff => [| diff IHdiff] i j /=. + move/eqP; rewrite -/(leq j i) => H1 /andP[H2 Hj]. by rewrite (_ : i = j); last by apply/eqP; rewrite eqn_leq H1 H2. + move=> Hdiff => /andP[_ Hj]. have Hiltj : i < j by rewrite -subn_gt0 Hdiff. apply: (Rtrans (y := nth Z r i.+1)). * by apply: H; exact: (leq_ltn_trans Hiltj). * apply: IHdiff => //=; first by rewrite subnS Hdiff. by rewrite Hiltj Hj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)