proposition: Theorem ZDividesLe : forall n m : Z, n <> 0%Z -> Zdivides n m -> (Z.abs m <= Z.abs n)%Z.
proof: Proof. intros n m H' H'0; case H'0; intros q E; rewrite E. rewrite Zabs_Zmult. pattern (Z.abs m) at 1 in |- *; replace (Z.abs m) with (Z.abs m * 1)%Z; [ idtac | ring ]. apply Zle_Zmult_comp_l; auto with zarith. generalize E H'; case q; simpl in |- *; auto; try (intros H1 H2; case H2; rewrite H1; ring; fail); intros p; case p; unfold Z.le in |- *; simpl in |- *; intros; red in |- *; discriminate. Qed.
imports: Reals ZArith List PeanoNat Psatz