0 ≤ d * d

Stream: new members

[Jiekai]

example (d : ℤ): 0 ≤ d * d :=
begin
  sorry
end

Practicing with doc searching with no luck...

[Kevin Buzzard]

Guess: docs#mul_self_nonneg or docs#pow_two_nonneg

[Kevin Buzzard]

They're both there and it looks like the first one is the one you want (the second one was me playing it safe because I know there's a lemma saying $d\times d=d^2$)

[Kevin Buzzard]

Type class inference should fill in the fact that the integers are a totally ordered ring