Prove that for every number there is a prime larger than it

[lukacslacko]

The brief English proof goes like this: take a prime divisor p of n!+1, if p would be less than or equal to n, then p would divide n!, but then it could not divide n! + 1, thus n < p.

My plan to formalize this is:

• a lambda called x; y | divides which is true if 0<y and there is an M so that x*M=y.
• a few theorems as needed, like x; y | divides => x<=y, x; y | divides => 1 <= x, x;y|divides => y;z|divides => x;z|divides, x;y|divides => x;a*y|divides.
• a theorem which is feel at least as complicated as proving that even numbers follow odd ones and odd ones follow even ones, that if x; y | divides and 2 <= x => ~x; Sy | divides, so I guess we'll still need Prove that y<=x or x<= y #20 because it feels like that will lead to proving that odd/even follows even/odd, so probably the same thing will be needed for this too.
• a lambda called x.is_prime which is true if 2 <= x and !d(d; x|divides => d=1 or d=x)
• some examples, like 2.is_prime, 3.is_prime, ~4.is_prime, 2<=x => 2<=y => ~(x*y).is_prime
• a theorem which says that 2<=x => ~!p~p;x|divides and p.is_prime. I think it goes that way that if x is a prime, then we're good, otherwise there is a divisor which is less than x but larger than 1, and one can apply the induction hypothesis on it.
• I don't really know how to define factorial, but one can at least say that !x ~!y~ !z 1<=z => z <=x => z;y | divides, that is, for every x there is a number y which is divisible by every number from 1 to x, and prove this by induction, by taking the (Sx)*y as the evidence for Sx if y is the evidence for x.
• With all these, I think we can then combine these together to prove what we want.