proposition: Lemma inj_div n m : N.to_nat (n / m) = N.to_nat n / N.to_nat m.
proof: Proof. destruct m as [|m]; [now destruct n|]. apply Nat.div_unique with (N.to_nat (n mod (N.pos m))). - apply Nat.compare_lt_iff. rewrite <- inj_compare. now apply N.mod_lt. - now rewrite <- inj_mul, <- inj_add, <- N.div_mod. Qed.
imports: BinPos BinNat PeanoNat Pnat