proposition: Lemma SF_lx_rcons (s : SF_seq) (h : R*T) : SF_lx (SF_rcons s h) = rcons (SF_lx s) (fst h).
proof: Proof. case: s => sh st ; rewrite /SF_lx /SF_rcons /= ; elim: st sh => // [[x y] st] IHst sh /= ; by rewrite (IHst x). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy