proposition: Lemma quot_abs_r : forall a b, b ~= 0 -> a÷(abs b) == (sgn b)*(a÷b).
proof: Proof. intros a b Hb. destruct (lt_trichotomy 0 b) as [LT|[EQ|LT]]. - rewrite abs_eq, sgn_pos by order. now nzsimpl. - order. - rewrite abs_neq, quot_opp_r, sgn_neg by order. rewrite mul_opp_l. now nzsimpl. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv