proposition: Lemma SF_size_f1 {T : Type} (f1 : R -> T) P : SF_size (SF_seq_f1 f1 P) = Peano.pred (size P).
proof: Proof. case: P => [| h P] //= ; by rewrite /SF_size /= size_pairmap. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy