proposition: Lemma rem_abs_r : forall a b, b ~= 0 -> a rem (abs b) == a rem b.
proof: Proof. intros a b Hb. destruct (le_ge_cases 0 b). - now rewrite abs_eq. - now rewrite abs_neq, ?rem_opp_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv