proposition: Lemma SF_cons_rcons (h : R*T) (s : SF_seq) (l : R*T) : SF_cons h (SF_rcons s l) = SF_rcons (SF_cons h s) l.
proof: Proof. case: h => hx hy ; case: l => lx ly ; case: s => sh st //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy