proposition: Lemma quot_same : forall a, a~=0 -> a÷a == 1.
proof: Proof. intros a ?. pos_or_neg a. - apply NZQuot.div_same; order. - rewrite <- quot_opp_opp by trivial. now apply NZQuot.div_same. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv