∀x,y:ℤ. uiff(¬(x ≤ y);y < x)
{ ((UnivCD THENA Auto) THEN Decide y < x THEN Auto) }
1. x : ℤ@i
2. y : ℤ@i
3. y < x
4. y < x
⊢ ¬(x ≤ y)
3. ¬y < x
4. ¬(x ≤ y)
⊢ y < x