proposition: Lemma inj_quot n m : 0<=n -> 0<=m -> Z.to_N (n÷m) = (Z.to_N n / Z.to_N m)%N.
proof: Proof. destruct m. - now destruct n. - intros. now rewrite Z.quot_div_nonneg, inj_div. - now destruct 2. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat