Commit 2024-07-01 15:55 63bddcd1

View on Github →

chore(Data/PNat): drop bit* lemmas (#14217) Add OfNat lemmas instead.

Estimated changes

deleted theorem PNat.bit0_le_bit0
deleted theorem PNat.bit0_le_bit1
deleted theorem PNat.bit1_le_bit0
deleted theorem PNat.bit1_le_bit1
added theorem PNat.ofNat_inj
added theorem PNat.ofNat_le_ofNat
added theorem PNat.ofNat_lt_ofNat