proposition: Lemma BZ_0_if_val0 x: intp x -> BZ_val x = \0c -> x = \0z.
proof: Proof. move /candu2P => [pa]; case; first by move => [] /setC1_P []. move => [_ pb] pc; rewrite/BZ_zero /BZ_of_nat; apply: pair_exten;aw; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)