proposition: Lemma mod_bound_abs : forall a b, b~=0 -> abs (a mod b) < abs b.
proof: Proof. intros a b **. destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ. - destruct (mod_pos_bound a b). + order. + now rewrite abs_eq. - destruct (mod_neg_bound a b). + order. + rewrite abs_neq; trivial. now rewrite <- opp_lt_mono. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv