proposition: Lemma SF_ly_f1 {T : Type} (f1 : R -> T) P : SF_ly (SF_seq_f1 f1 P) = Rcomplements.belast (map f1 P).
proof: Proof. case: P => [| h P] // ; elim: P h => //= h P IH h0 ; by rewrite -(IH h). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy