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