proposition: Lemma BZprod_1_inversion_l x y : intp x -> intp y -> x *z y = \1z -> (x = y /\ (x = \1z \/ x = \1mz)).
proof: Proof. move => xz yz eq1. move: (sym_eq (BZprod_val x y)); rewrite eq1 BZ_of_nat_val => eq2. move :(BZ_valN xz) (BZ_valN yz) => pa pb. move:(cprod_eq1 (CS_nat pa) (CS_nat pb) eq2) => [ea eb]. move /candu2P: xz => [prx]; case; move => [_ h]. have x1: x = \1mz by rewrite /BZ_mone/BZm_of_nat(Y_false card1_nz) -prx ea h. move: (BZprod_m1l yz); rewrite - x1 eq1 {1} x1 - BZopp_1 => ->. by rewrite (BZopp_K yz); split => //; right. have x1: x = \1z by rewrite /BZ_one/BZ_of_nat;apply:pair_exten; fprops; aw. by move: eq1; rewrite x1 (BZprod_1l yz) => ->; split => //; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)