Just noting that the statement in question is not only a valid proposition in intuitionistic logic, but also in classical logic. That's not really surprising, a

Just noting that the statement in question is not only a valid proposition in intuitionistic logic, but also in classical logic. That's not really surprising, as classical logic can prove everything that intuitionism can prove, but it deserves to be called out, as it otherwise might seem more sophisticated than it is for people unfamiliar with the finer details of proof systems.