let n be Nat; :: thesis: n \/ {n} = n + 1
n + 1 = succ n ;
hence n \/ {n} = n + 1 ; :: thesis: verum