proposition: Lemma SF_cat_pointed (x y : SF_seq) : last (SF_h x) (SF_lx x) = head (SF_h y) (SF_lx y) -> pointed_subdiv x -> pointed_subdiv y -> pointed_subdiv (SF_cat x y).
proof: Proof. intros Hxy Hx Hy. move: Hxy Hx. apply (SF_cons_ind (fun x => last (SF_h x) (SF_lx x) = head (SF_h y) (SF_lx y) -> pointed_subdiv x -> pointed_subdiv (SF_cat x y))) => {x} /= [x0 | x0 x IH] Hxy Hx. rewrite Hxy. by apply Hy. rewrite -SF_cons_cat. case => [ | i] Hi. apply (Hx O), Nat.lt_0_succ. apply IH =>//. by apply ptd_cons with x0. by apply <-Nat.succ_lt_mono; apply Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy