proposition: Lemma last_inv A B (f : A -> B) (x1 x2 : A) (h : seq A) : f x1 = f x2 -> f (last x1 h) = f (last x2 h).
proof: Proof. by elim: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep