proposition: Lemma z_infinite_nat: z_infinite (IM nat_to_B).
proof: Proof. split; first by apply/IM_P; exists 0. move => x /IM_P [n ->]; apply/IM_P; exists n.+1. by rewrite /= (succ_of_nat (nat_to_B_Nat n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)