proposition: Lemma SF_last_cat (x y : SF_seq) : last (SF_h x) (SF_lx x) = head (SF_h y) (SF_lx y) -> last (SF_h (SF_cat x y)) (SF_lx (SF_cat x y)) = (last (SF_h y) (SF_lx y)).
proof: Proof. rewrite SF_lx_cat. unfold SF_cat, SF_lx ; simpl => <- /=. elim: (SF_t x) (SF_h x) => //= {x} x1 x x0. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy