proposition: Lemma last_unzip1 {S T} x0 y0 (s : seq (S * T)) : last x0 (unzip1 s) = fst (last (x0,y0) s).
proof: Proof. case: s => [ | h s] //= . elim: s h => [ | h0 s IH] h //=. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy