proposition: Lemma lfun1_poly (p : {poly aT}) : map_poly \1%VF p = p.
proof: Proof. by apply: map_poly_id => u _; apply: id_lfunE. 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)