proposition: Lemma seq_cut_up_head' (s : seq (R*R)) x x0 z : fst (head z (seq_cut_up' s x x0)) = x.
proof: Proof. elim: s z x0 => [ | x1 s IH] //= z x0. by case: Rle_dec. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy