proposition: Lemma floorpK : {in polyOver int_num, cancel (map_poly floor) (map_poly intr)}.
proof: Proof. move=> p /(all_nthP 0) Zp; apply/polyP=> i. rewrite coef_map coef_map_id0 //= -[p]coefK coef_poly. by case: ifP => [/Zp/floorK // | _]; rewrite floor0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)