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