proposition: Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
proof: Proof. intros [x|x] [y|y]; simpl; symmetry; rewrite NN.spec_div; destruct (Z.eq_dec (NN.to_Z y) 0) as [EQ|NEQ]; try (rewrite EQ; now destruct (NN.to_Z x)); rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; trivial; apply Z.quot_div_nonneg; generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig