proposition: Lemma SF_size_lx (s : SF_seq) : size (SF_lx s) = S (SF_size s).
proof: Proof. case: s => sh st ; rewrite /SF_size /= ; elim: st => //= _ st -> //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy