proposition: Lemma SF_map_f1 {T T0 : Type} (f : T -> T0) (f1 : R -> T) P : SF_map f (SF_seq_f1 f1 P) = SF_seq_f1 (fun x => f (f1 x)) P.
proof: Proof. case: P => [| h P] // ; elim: P h => [| h0 P IH] h //. rewrite ?(SF_cons_f1 _ _ (h0::P)) /= ; try intuition. rewrite SF_map_cons IH ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy