proposition: Fact int_num_subring : subring_closed int_num.
proof: Proof. by split=> // _ _ /intrP[n ->] /intrP[m ->]; rewrite -?mulrzBr -?intrM intr_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)