[mizar] n > 0 vs n <> 0

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Dear All,

recently I was working with non empty natural numbers and I always had an
assumption n <> 0. But, many related theorems already stored in the MML
have an assumption n > 0. To use them one has to do an extra step referring
to NAT_1:19. Moreover, n <> 0 is simpler than n > 0.

Then I would propose to make a revision of the MML changing all
assumptions n > 0 into n <> 0.

But, I recognized one problem:

theorem Th10: ::GR_CY_1:10
for n,s being natural number st n > 0 holds s in Segm (n) iff s < n;

theorem Th12: ::GR_CY_1:12
for n being natural number st n > 0 holds 0 in Segm (n) by Th10;

In present MML, Th12 is a trivial consequence of Th10. But if we change
n > 0 into n <> 0, then Th12 needs more complex proof. The reason is that
predicate symbol < disappeared.

The question is: when Library Committee agrees to do the revision should
we leave Th10 and Th12 (and other similar cases) as are, or should we
prove them.

Greetings
Artur Kornilowicz