proposition: Lemma inj_mod n m : 0<=n -> 0<=m -> Z.to_N (n mod m) = ((Z.to_N n) mod (Z.to_N m))%N.
proof: Proof. destruct n, m; trivial; intros Hn Hm; (now destruct Hn) || (now destruct Hm) || clear. simpl. rewrite <- (N2Z.id (_ mod _)). f_equal. now rewrite N2Z.inj_mod. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat