proposition: Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
proof: Proof. intros. rewrite (div_mod a b) at 1; try order. rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv