proposition: Lemma SF_rev_0 (s : SF_seq) : size (rev (SF_lx s)) = S (size (rev (SF_ly s))).
proof: Proof. by rewrite ?size_rev SF_size_lx SF_size_ly. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy