proposition: Lemma BZprod_1_inversion_s x y : intp x -> intp y -> x *z y = \1z -> (BZabs y = \1z).
proof: Proof. move => pa pb pc; move:(BZprod_1_inversion_l pa pb pc) => [->]. by case => ->; rewrite ? BZabs_1 ? BZabs_m1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)