proposition: Lemma inj_mod n m : 0<=n -> 0<=m -> Z.to_nat (n mod m) = (Z.to_nat n mod Z.to_nat m)%nat.
proof: Proof. intros. now rewrite <- !Z_N_nat, Z2N.inj_mod, N2Nat.inj_mod. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat