proposition: Lemma rem_abs_l : forall a b, b ~= 0 -> (abs a) rem b == abs (a rem b).
proof: Proof. intros a b Hb. destruct (le_ge_cases 0 a) as [LE|LE]. - rewrite 2 abs_eq; try easy. now apply rem_nonneg. - rewrite 2 abs_neq, rem_opp_l; try easy. now apply rem_nonpos. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv