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