proposition: Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<b \/ b<a<=0).
proof: Proof. intros a b **. rewrite <- div_small_iff, mod_eq by trivial. rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l. rewrite eq_sym_iff, eq_mul_0. tauto. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv