proposition: Lemma SF_fun_map {T T0 : Type} (f : T -> T0) (s : SF_seq) y0 : forall x, SF_fun (SF_map f s) (f y0) x = f (SF_fun s y0 x).
proof: Proof. case: s => sh st ; rewrite /SF_fun /SF_map /= ; case: st => [| h st] x /=. by case: Rle_dec. case: Rlt_dec => //. elim: st sh h y0 x => [| h0 st IH] sh h y0 x Hx //=. by case: Rle_dec. case: Rlt_dec => // {} Hx. by apply: (IH (fst h)). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy