Commit 2024-04-28 14:16 7a11b9f3

View on Github →

feat(PNat/Basic): add three lemmas (#12479) Three small lemmata in support of further PNat proofs

Estimated changes

added theorem PNat.add_one
added theorem PNat.lt_succ_self
added theorem PNat.one_lt_of_lt