proposition: Lemma sorted_nth {T : Type} (Ord : T -> T -> Prop) (s : seq T) : sorted Ord s <-> (forall i : nat, (i < Peano.pred (size s))%nat -> forall x0 : T, Ord (nth x0 s i) (nth x0 s (S i))).
proof: Proof. case: s. split => // _ i Hi ; contradict Hi ; apply Nat.nlt_0_r. move => t s ; elim: s t => [ t | t s IHs t0] ; split => // H. move => i Hi ; contradict Hi ; apply Nat.nlt_0_r. case => [| i] Hi x0 ; simpl in Hi. apply H. case: (IHs t) => {} IHs _ ; apply (IHs (proj2 H) i (proj2 (Nat.succ_lt_mono _ _) Hi) x0). split. apply (H O (Nat.lt_0_succ _) t). case: (IHs t) => {IHs} _ IHs. apply: IHs => i Hi x0 ; apply: (H (S i)) ; simpl ; apply ->Nat.succ_lt_mono. now apply Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy