proposition: Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a.
proof: Proof. intros a b ?. pos_or_neg a; pos_or_neg b. - apply NZQuot.div_mul; order. - rewrite <- quot_opp_opp, <- mul_opp_r by order. apply NZQuot.div_mul; order. - rewrite <- opp_inj_wd, <- quot_opp_l, <- mul_opp_l by order. apply NZQuot.div_mul; order. - rewrite <- opp_inj_wd, <- quot_opp_r, <- mul_opp_opp by order. apply NZQuot.div_mul; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv