Theorem PNat.ofNat_lt_ofNat

Modification history