take 0 ; :: thesis: 0 is natural
thus 0 is natural ; :: thesis: verum