proposition: Lemma inj_mul_abs n m : Z.abs_nat (Z.abs n * Z.abs m) = (Z.abs_nat n * Z.abs_nat m)%nat.
proof: Proof. now rewrite <- !Zabs_N_nat, Zabs2N.inj_mul_abs, N2Nat.inj_mul. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat