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