proposition: Lemma SF_rcons_dec (P : SF_seq -> Type) : (forall x0 : R, P (SF_nil x0)) -> (forall s t, P (SF_rcons s t)) -> (forall s, P s).
proof: Proof. move => Hnil Hrcons [sh st] ; move: st ; apply rcons_dec => [| st t]. apply Hnil. apply (Hrcons (mkSF_seq sh st) t). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy