proposition: Lemma SF_map_cons (f : T -> T0) (h : R*T) (s : SF_seq) : SF_map f (SF_cons h s) = SF_cons (fst h, f (snd h)) (SF_map f s).
proof: Proof. case: s => sh ; elim => // h st ; rewrite /SF_map => //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy