Commit 2024-06-17 08:52 9cbd6ff1

View on Github →

feat: add missing WithTop/WithBot lemmas and improve WithBot Nat proofs (#13884)

Estimated changes

added theorem WithBot.bot_ne_ofNat
added theorem WithBot.coe_eq_ofNat
added theorem WithBot.coe_ofNat
added theorem WithBot.ofNat_eq_coe
added theorem WithBot.ofNat_ne_bot
added theorem WithTop.coe_eq_ofNat
added theorem WithTop.coe_ofNat
added theorem WithTop.ofNat_eq_coe
added theorem WithTop.ofNat_ne_top
added theorem WithTop.top_ne_ofNat