proposition: Lemma BZprod_m1r x: intp x -> x *z \1mz = BZopp x.
proof: Proof. move => xz; move: (CS_nat (BZ_valN xz)) => h. rewrite BZprodE /BZprod_int /BZ_mone /BZm_of_nat /BZ_of_nat /BZopp/int_np. by rewrite (Y_false card1_nz); aw; rewrite cprod1r//; Ytac0; Ytac aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)