## Stream: new members

### Topic: 1/2 > 0

#### Debendro Mookerjee (Apr 01 2020 at 15:15):

How do you prove that 1/2 > 0
?

#### Reid Barton (Apr 01 2020 at 15:15):

(a) the norm_num tactic; (b) it might not be true.

#### Johan Commelin (Apr 01 2020 at 15:18):

@Debendro Mookerjee This depends on where the division takes place...

#### Johan Commelin (Apr 01 2020 at 15:18):

1/2 = 0 in the natural numbers.

in the reals

#### Kenny Lau (Apr 01 2020 at 15:20):

it should be half_pos iirc

one_half_pos

#### Kevin Buzzard (Apr 01 2020 at 16:36):

But the best answer is norm_num, a generic tactic which will prove any equality or inequality for explicit real numbers.

Last updated: May 16 2021 at 05:21 UTC