proposition: Lemma nth_belast_0 (I : eqType ) (l : seq I) i j : 0 < size l -> nth i (belast j l) 0 = j.
proof: Proof. by case: l. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound