proposition: Lemma intrE x : (x \is a int_num) = (x \is a nat_num) || (- x \is a nat_num).
proof: Proof. exact: Num.int_num_subproof. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)