proposition: Lemma ptd_cons h s : pointed_subdiv (SF_cons h s) -> pointed_subdiv s.
proof: Proof. move => H i Hi ; apply (H (S i)) ; rewrite SF_size_cons ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy