proposition: Lemma last1_neq0 (R : ringType) (s : seq R) (c : R) : c != 0 -> (last c s != 0) = (last 1 s != 0).
proof: Proof. by elim: s c => [|t s ihs] c cn0 //; rewrite oner_eq0 cn0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)