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