proposition: Lemma inj_mod n m : Z.of_nat (n mod m) = (Z.of_nat n mod Z.of_nat m)%Z.
proof: Proof. destruct m as [|m]; [now destruct n|]. now rewrite <- !nat_N_Z, Nat2N.inj_mod, N2Z.inj_mod. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat