proposition: Lemma SF_map_rcons (f : T -> T0) (s : SF_seq) (h : R*T) : SF_map f (SF_rcons s h) = SF_rcons (SF_map f s) (fst h, f (snd h)).
proof: Proof. move: h ; apply SF_cons_ind with (s := s) => {s} [x0 | h0 s IH] //= h. rewrite SF_map_cons. replace (SF_rcons (SF_cons h0 s) h) with (SF_cons h0 (SF_rcons s h)) by auto. rewrite SF_map_cons. rewrite IH. auto. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy