proposition: Lemma SF_ly_f2 {T : Type} (f2 : R -> R -> T) P : SF_ly (SF_seq_f2 f2 P) = behead (pairmap f2 0 P).
proof: Proof. case: P => [| h P] // ; elim: P h => //= h P IH h0 ; by rewrite -(IH h). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy