proposition: Lemma floorpP (p : {poly R}) : p \is a polyOver int_num -> {q | p = map_poly intr q}.
proof: Proof. by exists (map_poly floor p); rewrite floorpK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)