proposition: Lemma inj_div n m : 0<=n -> 0<=m -> Z.to_N (n/m) = (Z.to_N n / 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 (_ / _)). f_equal. now rewrite N2Z.inj_div. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat