proposition: Lemma BZms_hi_pr x: inc x BZms -> (BZ_val x <> \0c /\ BZm_of_nat (BZ_val x) = x).
proof: Proof. move /indexed_P => [pa] /setC1_P [pb pc] pd;split => //. by rewrite /BZm_of_nat; Ytac0; rewrite - {2} pa pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)