proposition: Lemma intrP x : reflect (exists m, x = m%:~R) (x \is a int_num).
proof: Proof. apply: (iffP idP) => [x_int | [m -> //]]. rewrite -[x]opprK; move: x_int; rewrite intrE. move=> /orP[] /natrP[n ->]; first by exists n; rewrite opprK. by exists (- n%:R); rewrite mulrNz mulrz_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)