Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 1 subgoal
- x : Z
- y : Z
- H_mod : x mod 2 = y mod 2
- i : Z
- j : Z
- H_t : True
- H_le : i < j -> (x + y) / 2 - i = j - (x + y) / 2
- H_gt : i >= j -> (x + y) / 2 - j = i - (x + y) / 2
- H_ij : i <> j
- H_lt : i < j
- i0 : Z
- H_i0 : i0 = i + 1
- j0 : Z
- H_j0 : j0 = j - 1
- ============================
- 0 < 0
Add Comment
Please, Sign In to add comment
