proposition: Lemma BZprod_1l x: intp x -> \1z *z x = x.
proof: Proof. move => xz; move: (CS_nat (BZ_valN xz)) => cpx. rewrite BZprodE /BZprod_int /BZ_one /BZ_of_nat /BZopp/int_np. aw; rewrite cprod1l //;Ytac0. case /BZ_i0P: xz => h. by rewrite (BZms_sg h); Ytac0; apply:BZm_hi_pr; apply:BZms_sBZm. by rewrite (BZp_sg h); Ytac0; apply:BZp_hi_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)