proposition: Lemma seq_step_rev (l : seq R) : seq_step (rev l) = seq_step l.
proof: Proof. rewrite /seq_step. rewrite head_rev behead_rev /=. case: l => [ | x0 l] //=. case: l => [ | x1 l] //=. rewrite rev_cons. case: l => [ | x2 l] //=. by rewrite -Rabs_Ropp Ropp_minus_distr'. rewrite rev_cons pairmap_rcons foldr_rcons. rewrite -Rabs_Ropp Ropp_minus_distr'. generalize (Rabs (x1 - x0)) ; clear. elim: l x1 x2 => [ | x2 l IH] x0 x1 r //=. rewrite -Rabs_Ropp Ropp_minus_distr' !Rmax_assoc. apply f_equal2 => //. by apply Rmax_comm. rewrite rev_cons pairmap_rcons foldr_rcons. rewrite -Rabs_Ropp Ropp_minus_distr' Rmax_assoc IH. by rewrite (Rmax_comm _ r) !Rmax_assoc. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy