proposition: Lemma SF_cons_ind (P : SF_seq -> Type) : (forall x0 : R, P (SF_nil x0)) -> (forall h s, P s -> P (SF_cons h s)) -> (forall s, P s).
proof: Proof. move => Hnil Hcons [sh st] ; elim: st sh => [sh |h sf IHst sh]. apply Hnil. move: (IHst (fst h)) => {} IHst. move: (Hcons (sh,snd h) (mkSF_seq (fst h) sf) IHst) => {Hcons} ; rewrite /SF_cons -surjective_pairing //=. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy