proposition: Lemma SF_size_cons (h : R*T) (s : SF_seq) : SF_size (SF_cons h s) = S (SF_size s).
proof: Proof. rewrite /SF_cons /SF_size //=. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy