Where are instances of ZeroLEOneClass and PosMulMono for ℤ

Stream: new members

[Kevin Cheung]

I am trying to trim down the imports for the following as much as possible:

import Mathlib.Data.Int.Star

set_option autoImplicit false

example (a : ℤ) : 0 ≤ a ^ 2 := by apply sq_nonneg

Starting with the following,

import Mathlib.Algebra.Order.Ring.Unbundled.Basic
import Mathlib.Algebra.Ring.Int -- for Semiring ℤ

set_option autoImplicit false

example (a : ℤ) : 0 ≤ a ^ 2 := by
  apply?

I got the suggestion

Try this: refine sq_nonneg a
Remaining subgoals:
⊢ ZeroLEOneClass ℤ
⊢ PosMulMono ℤ

Accepting the suggestion gave the following error:

failed to synthesize
  ZeroLEOneClass ℤ
Additional diagnostic information may be available using the `set_option diagnostics true` command.

I think I need imports containing instances of ZeroLEOneClass and PosMulMono for ℤ. But I was unable to find anything other than Mathlib.Data.Int.Star that makes it work. Help or pointers greatly appreciated.

[Yakov Pechersky]

I think this works currently

import Mathlib.Algebra.Order.Ring.Int

lemma foo (z : ℤ) : 0 ≤ z ^ 2 := by apply? says exact sq_nonneg z

#min_imports -- import Mathlib.Algebra.Order.Ring.Int

[Kevin Cheung]

Thank you.