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