proposition: Lemma quot_abs : forall a b, b ~= 0 -> (abs a)÷(abs b) == abs (a÷b).
proof: Proof. intros a b Hb. pos_or_neg a; [rewrite (abs_eq a)|rewrite (abs_neq a)]; try apply opp_nonneg_nonpos; try order. - pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)]; try apply opp_nonneg_nonpos; try order. + rewrite abs_eq; try easy. apply NZQuot.div_pos; order. + rewrite <- abs_opp, <- quot_opp_r, abs_eq; try easy. apply NZQuot.div_pos; order. - pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)]; try apply opp_nonneg_nonpos; try order. + rewrite <- (abs_opp (_÷_)), <- quot_opp_l, abs_eq; try easy. apply NZQuot.div_pos; order. + rewrite <- (quot_opp_opp a b), abs_eq; try easy. apply NZQuot.div_pos; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv