proposition: Lemma seq_step_ge_0 x : (0 <= seq_step x).
proof: Proof. clear ; unfold seq_step ; case: x => [ | x0 x] //= . by apply Rle_refl. elim: x x0 => [ | x1 x IH] //= x0. by apply Rle_refl. apply Rmax_case. by apply Rabs_pos. by []. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy