proposition: Lemma inj_rem n m : Z.abs_N (Z.rem n m) = ((Z.abs_N n) mod (Z.abs_N m))%N.
proof: Proof. assert (forall p q, Z.abs_N (Z.rem (Zpos p) (Zpos q)) = ((Npos p) mod (Npos q))%N). { intros. rewrite abs_N_nonneg. - now apply Z2N.inj_rem. - now apply Z.rem_nonneg. } destruct n, m; trivial; simpl. - now rewrite <- Pos2Z.opp_pos, Z.rem_opp_r. - now rewrite <- Pos2Z.opp_pos, Z.rem_opp_l, inj_opp. - now rewrite <- 2 Pos2Z.opp_pos, Z.rem_opp_opp, inj_opp. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat