Commit 2026-02-23 17:11 1d41459a
View on Github →feat(Data/Nat/SuccPred): m ⋖ n ↔ m + 1 = n (#34806)
This is a special case of a general lemma which can't be simp. Also turn Fin.coe_covBy_iff around to preserve confluence.
From ProofBench
feat(Data/Nat/SuccPred): m ⋖ n ↔ m + 1 = n (#34806)
This is a special case of a general lemma which can't be simp. Also turn Fin.coe_covBy_iff around to preserve confluence.
From ProofBench