proposition: Lemma rem_mod : forall a b, b~=0 -> a rem b == (sgn a) * ((abs a) mod (abs b)).
proof: Proof. intros a b Hb. rewrite <- rem_abs_r by trivial. assert (Hb' := proj2 (abs_pos b) Hb). destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]]. - rewrite (abs_eq a), sgn_pos, mul_1_l, rem_mod_nonneg; order. - rewrite <- Ha, abs_0, sgn_0, mod_0_l, rem_0_l, mul_0_l; order. - rewrite sgn_neg, (abs_neq a), mul_opp_l, mul_1_l, eq_opp_r, <-rem_opp_l by order. apply rem_mod_nonneg; trivial. apply opp_nonneg_nonpos; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor