proposition: Lemma inj_quot n m : Z.abs_N (n÷m) = ((Z.abs_N n) / (Z.abs_N m))%N.
proof: Proof. assert (forall p q, Z.abs_N (Zpos p ÷ Zpos q) = (Npos p / Npos q)%N). { intros. rewrite abs_N_nonneg. - now apply Z2N.inj_quot. - now apply Z.quot_pos. } destruct n, m; trivial; simpl. - now rewrite <- Pos2Z.opp_pos, Z.quot_opp_r, inj_opp. - now rewrite <- Pos2Z.opp_pos, Z.quot_opp_l, inj_opp. - now rewrite <- 2 Pos2Z.opp_pos, Z.quot_opp_opp. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat