proposition: Lemma BZm_of_natm_i x: natp x -> inc (BZm_of_nat x) BZm.
proof: Proof. move => xN; rewrite /BZm_of_nat; Ytac xnz; first by apply /setU1_P; right. by apply /setU1_P; left; apply: indexed_pi; apply /setC1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)