proposition: Lemma inj_rem n m :0<=n -> 0<=m -> Z.to_N (Z.rem n m) = ((Z.to_N n) mod (Z.to_N m))%N.
proof: Proof. destruct m. - now destruct n. - intros. now rewrite Z.rem_mod_nonneg, inj_mod. - now destruct 2. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat