theorem :: NAT_6:33

5 is Proth