Commit 2024-05-02 08:30 40cac78d

View on Github →

feat(PNat/Basic): two small sub/le lemmata (#12492)

Estimated changes

added theorem PNat.le_sub_one_of_lt
added theorem PNat.sub_le