proposition: Lemma int_in_NP x: reflect (exists n, x = n%:Z) (int_in_N x).
proof: Proof. apply:(iffP idP) => [h | [n ->]]; first by exists (absz x); apply/eqP. apply:int_in_N_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)