proposition: Lemma SF_lx_cat (x y : SF_seq) : SF_lx (SF_cat x y) = (SF_lx x) ++ (behead (SF_lx y)).
proof: Proof. unfold SF_cat, SF_lx ; simpl. apply f_equal. by elim: (SF_t x) => //= t h ->. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy