proposition: Lemma ptd_sort ptd : pointed_subdiv ptd -> SF_sorted Rle 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 y0 ; apply (Hptd O) ; rewrite SF_size_cons ; apply Nat.lt_0_succ. apply Rle_trans with y0 ; apply (Hptd O) ; rewrite SF_size_cons ; apply Nat.lt_0_succ. apply IH, (ptd_cons (x0,y0)) => //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy