proposition: Lemma inj_rem n m : Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m).
proof: Proof. destruct m. - now destruct n. - rewrite Z.rem_mod_nonneg, inj_mod; trivial. + apply is_nonneg. + easy. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat