proposition: Lemma BZ_hi_pr a: intp a -> a = BZ_of_nat (BZ_val a) \/ a = BZm_of_nat (BZ_val a).
proof: Proof. move /candu2P => [pa] [] [pb pc]. right; symmetry; apply:BZm_hi_pr; apply /setU1_P; left. by apply/ indexed_P. by left; symmetry; apply BZp_hi_pr; apply/ indexed_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)