Commit 2023-01-26 13:42 23df7e4a

View on Github →

feat: port Data.ENat.Basic (#1531)

Estimated changes

added theorem ENat.add_one_le_iff
added theorem ENat.add_one_le_of_lt
added theorem ENat.coe_add
added theorem ENat.coe_mul
added theorem ENat.coe_ne_top
added theorem ENat.coe_one
added theorem ENat.coe_sub
added theorem ENat.coe_toNat_eq_self
added theorem ENat.coe_toNat_le_self
added theorem ENat.coe_zero
added theorem ENat.le_of_lt_add_one
added theorem ENat.nat_induction
added def ENat.ofNat
added theorem ENat.one_le_iff_pos
added def ENat.recTopCoe
added theorem ENat.recTopCoe_coe
added theorem ENat.recTopCoe_top
added theorem ENat.sub_top
added theorem ENat.succ_def
added def ENat.toNat
added theorem ENat.toNat_add
added theorem ENat.toNat_coe
added theorem ENat.toNat_eq_iff
added theorem ENat.toNat_sub
added theorem ENat.toNat_top
added theorem ENat.top_ne_coe
added theorem ENat.top_sub_coe
added def ENat