proposition: Lemma inj_div n m : Z.of_N (n/m) = Z.of_N n / Z.of_N m.
proof: Proof. destruct m as [|m]. - now destruct n. - apply Z.div_unique_pos with (Z.of_N (n mod (Npos m))). + split. * apply is_nonneg. * apply inj_lt. now apply N.mod_lt. + rewrite <- inj_mul, <- inj_add. f_equal. now apply N.div_mod. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat