proposition: Lemma BZ_ideal_unique_gen a b: intp a -> intp b -> BZ_ideal1 a = BZ_ideal1 b -> BZabs a = BZabs b.
proof: Proof. move => az bz sv. move: (BZ_in_ideal4 az) (BZ_in_ideal4 bz) => [pa pb] [_]. rewrite - sv => /funI_P [z zz eq1]. move: pb; rewrite sv => /funI_P [u uz]; rewrite eq1. rewrite - (BZprodA az zz uz) => aux. move: (BZprod_abs az zz); rewrite - eq1;move => ->. move: (ZSa az) => aaz. by case: (BZprod_1_inversion_more az zz uz aux); move => ->; rewrite? BZabs_1 ? BZabs_0 ?BZabs_m1 ?BZprod_0l // BZprod_1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)