Commit 2022-12-28 14:03 95f15947

View on Github →

Port/data.pnat.find (#1220) Port of data.pnat.find Also changed Nat.find_x to Nat.findX to follow naming conventions

Estimated changes

added theorem PNat.find_comp_succ
added theorem PNat.find_eq_iff
added theorem PNat.find_eq_one
added theorem PNat.find_le
added theorem PNat.find_le_iff
added theorem PNat.find_lt_iff
added theorem PNat.find_mono
added theorem PNat.le_find_iff
added theorem PNat.lt_find_iff
added theorem PNat.one_le_find