Nuprl - Pf div_2_to

(10steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

1. a: {...0}
2. b:
3. 0((-a) rem b)
4. ((-a) rem b) < b
5. 0(a rem b)
6. (a rem b) > -b
7. -a+-b((-a) b) = ((-a) rem b)
8. a+-b(a b) = (a rem b)

(a b) = -((-a) b)

By: RevHypSubst 7 3 THEN RevHypSubst 7 4 THEN RevHypSubst 8 5 THEN RevHypSubst 8 6 THEN OnHyps [8;7] Thin

Generated subgoal:

1 3. 0-a+-b((-a) b)
4. -a+-b((-a) b) < b
5. 0a+-b(a b)
6. a+-b(a b) > -b
(a b) = -((-a) b)

About:

(10steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc