proposition: Lemma SF_cons_f2 {T : Type} (f2 : R -> R -> T) (h : R) (P : seq R) : (0 < size P)%nat -> SF_seq_f2 f2 (h::P) = SF_cons (h,f2 h (head 0 P)) (SF_seq_f2 f2 P).
proof: Proof. case: P => [ H | h0 P _] //. by apply Nat.nlt_0_r in H. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy