proposition: Lemma nth_le_seq_step x0 (l : seq R) (i : nat) : (S i < size l)%nat -> Rabs (nth x0 l (S i) - nth x0 l i) <= seq_step l.
proof: Proof. elim: i l => [ | i IH] ; case => [ | x1 l] /= Hi. by apply Nat.nlt_0_r in Hi. apply Nat.succ_lt_mono in Hi. destruct l as [ | x2 l]. by apply Nat.nlt_0_r in Hi. by apply Rmax_l. by apply Nat.nlt_0_r in Hi. apply Nat.succ_lt_mono in Hi. move: (IH l Hi). destruct l as [ | x2 l] ; simpl. by apply Nat.nlt_0_r in Hi. simpl in Hi ; apply Nat.succ_lt_mono in Hi. move => {} IH. eapply Rle_trans. by apply IH. by apply Rmax_r. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy