theorem :: NAT_6:32

3 is Proth by Lm6;