proposition: Lemma head_rev {T} (x0 : T) (l : seq T) : head x0 (rev l) = last x0 l.
proof: Proof. elim: l x0 => /= [ | x1 l IH] x0. by []. by rewrite rev_cons head_rcons. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy