proposition: Lemma natrEint x : (x \is a nat_num) = (x \is a int_num) && (0 <= x).
proof: Proof. apply/idP/andP=> [Nx | [Zx x_ge0]]; first by rewrite intr_nat ?natr_ge0. by rewrite -(ger0_norm x_ge0) natr_norm_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)