proposition: Lemma inj_div n m : Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m.
proof: Proof. destruct m as [|m]; [now destruct n|]. now rewrite <- !nat_N_Z, Nat2N.inj_div, N2Z.inj_div. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat