## Stream: new members

### Topic: Automated tactic for solving trivial (in)equalities on reals

#### Donald Sebastian Leung (Feb 25 2020 at 07:06):

So I want to prove the following goal: (1 : ℝ) / 10 ≠ 1. Is there any automated tactic (in stdlib/mathlib) capable of solving the following goal immediately, or would I have to prove it from first principles?

#### Kevin Buzzard (Feb 25 2020 at 07:11):

Does norm_num work?

#### Donald Sebastian Leung (Feb 25 2020 at 08:20):

Kevin Buzzard said:

Does norm_num work?

That did the trick, thanks!

Last updated: May 11 2021 at 00:31 UTC