proposition: Lemma is_intE x : (denq x == 1) = is_nat x || is_nat (- x).
proof: Proof. by rewrite /is_nat denqN oppr_ge0 -andb_orl le_total. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)