proposition: Lemma polyOver1P p : reflect (exists q, p = map_poly (in_alg aT) q) (p \is a polyOver 1%VS).
proof: Proof. apply: (iffP idP) => [/allP/=Qp | [q ->]]; last first. by apply/polyOverP=> j; rewrite coef_map rpredZ ?memv_line. exists (map_poly (coord [tuple 1] 0) p). rewrite -map_poly_comp map_poly_id // => _ /Qp/vlineP[a ->] /=. by rewrite linearZ /= (coord_free 0) ?mulr1 // seq1_free ?oner_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)