proposition: Lemma sorted_compat (s : seq R) : sorted Rle s <-> RList.ordered_Rlist (s).
proof: Proof. case: s => [| h s]. split => // H i /= Hi ; contradict Hi ; apply Nat.nlt_0_r. elim: s h => [h | h s IHs h']. split => // H i /= Hi ; contradict Hi ; apply Nat.nlt_0_r. split => H. case => [ /= | i] ; rewrite size_compat => Hi ; simpl in Hi. apply H. apply (proj1 (IHs h) (proj2 H) i) ; rewrite size_compat /= ; apply Nat.lt_succ_r => //. split. apply (H O) ; rewrite size_compat /= ; apply Nat.lt_0_succ. apply IHs => i ; rewrite size_compat /= => Hi ; apply (H (S i)) ; rewrite size_compat /= ; apply ->Nat.succ_lt_mono; now apply Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy