proposition: Lemma SF_size_ly (s : SF_seq) : size (SF_ly 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