proposition: Lemma inj_quot n m : Z.of_N (n/m) = Z.of_N n ÷ Z.of_N m.
proof: Proof. destruct m. - now destruct n. - rewrite Z.quot_div_nonneg, inj_div; trivial. + apply is_nonneg. + easy. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat