proposition: Lemma SF_lx_f2 {T : Type} (f2 : R -> R -> T) P : (0 < size P)%nat -> SF_lx (SF_seq_f2 f2 P) = P.
proof: Proof. elim: P => [ H | h l IH _] //=. by apply Nat.nlt_0_r in H. case: l IH => [ | h' l] //= IH. rewrite -{2}IH //. by apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy