proposition: Lemma is_natE x : is_nat x = ((trunc x)%:R == x).
proof: Proof. rewrite /is_nat /trunc -numq_ge0 !rat_eq; case: (ratP x) => -[] //= n d pnd. rewrite pmulrn numq_int denq_int mulr1 -PoszM !eqz_nat -dvdn_eq. apply/eqP/idP => [->|/dvdnP[k nE]] //. by move/eqP: pnd; rewrite nE gcdnC gcdnMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)