Commit 2024-03-24 09:49 5d242aa4

View on Github →

fix: improve simp lemmas around PartENat.ofENat (#11553)

Estimated changes

added theorem PartENat.ofENat_coe
added theorem PartENat.ofENat_le
added theorem PartENat.ofENat_lt
deleted theorem PartENat.ofENat_none
added theorem PartENat.ofENat_ofNat
added theorem PartENat.ofENat_one
deleted theorem PartENat.ofENat_some
added theorem PartENat.ofENat_top
added theorem PartENat.ofENat_zero
modified theorem PartENat.withTopEquiv_le
modified theorem PartENat.withTopEquiv_lt
modified theorem PartENat.withTopEquiv_top