proposition: Lemma nth_compat (s : seq R) (n : nat) : RList.pos_Rl s n = nth 0 s n.
proof: Proof. elim: s n => [n|t s IHs n] /= ; case: n => //=. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy