proposition: Lemma BZ_ideal_unique_gen1 a b: inc a BZp -> inc b BZp -> BZ_ideal1 a = BZ_ideal1 b -> a = b.
proof: Proof. move => pa pb pc; move:(BZ_ideal_unique_gen (BZp_sBZ pa) (BZp_sBZ pb) pc). by rewrite (BZabs_pos pa) (BZabs_pos pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)