proposition: Theorem mod_le: forall a b, 0<=a -> b~=0 -> a mod b <= a.
proof: Proof. intros. pos_or_neg b. - apply mod_le; order. - rewrite <- mod_opp_r by trivial. apply mod_le; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv