proposition: Lemma SF_ly_rcons (s : SF_seq) (h : R*T) : SF_ly (SF_rcons s h) = rcons (SF_ly s) (snd h).
proof: Proof. case: s => sh st ; rewrite /SF_ly /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