proposition: Lemma ptd_sort' ptd : pointed_subdiv ptd -> sorted Rle (SF_ly ptd).
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} [x0 | [x0 y0] ptd] ; [ | apply SF_cons_dec with (s := ptd) => {ptd} [ x1 | [x1 y1] ptd] IH] => Hptd ; try split. apply Rle_trans with x1 ; [apply (Hptd O) | apply (Hptd 1%nat)] ; rewrite ?SF_size_cons ; repeat apply ->Nat.succ_lt_mono ; apply Nat.lt_0_succ. apply IH, (ptd_cons (x0,y0)) => //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy