>>11048037At an abstract level we want to prove that
forall x forall rational y [ p(x, y) => q(x, y) ]
Here p(x,y) is the statement that x is irrational
q(x, y) is the statement that x-y is irrational.
We do this by assuming that not(q(x,y)) and proving not(p(x, y))
forall x forall rational y [ p(x, y) => q(x, y) ]
is by the rule of transposition equivalent to
forall x forall rational y [not(q(x,y)) => not(p(x, y))]
So we got to prove that this holds for all x and y.
