proposition: Lemma seq_step_cat (x y : seq R) : (0 < size x)%nat -> (0 < size y)%nat -> last 0 x = head 0 y -> seq_step (cat x (behead y)) = Rmax (seq_step x) (seq_step y).
proof: Proof. case: x => /= [ H | x0 x _]. by apply Nat.lt_irrefl in H. case: y => /= [ H | y0 y _]. by apply Nat.lt_irrefl in H. move => <-. elim: x y x0 {y0} => /= [ | x1 x IH] y x0. rewrite {2}/seq_step /=. rewrite /Rmax ; case: Rle_dec (seq_step_ge_0 (x0 :: y)) => // _ _. unfold seq_step ; simpl. rewrite -Rmax_assoc. apply f_equal. by apply IH. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy