proposition: Lemma last_rev : forall s, last d (rev s) = head d s.
proof: Proof. by elim=> [//|s IHs]; rewrite rev_cons last_rcons. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2