Theorem Ordnode.Valid'.node4L_lemma₂

Modification history

2025-12-04 09:22

Mathlib/Data/Ordmap/Ordset.lean

feat(Tactic): add `lia` as an alias for `cutsat` and use it throughout (#32376) …

Modified Ordnode.Valid'.node4L_lemma₂ View on Github →

2025-09-24 05:32

Mathlib/Data/Ordmap/Ordset.lean

chore: replace omega with cutsat where possible (#29461) …

Modified Ordnode.Valid'.node4L_lemma₂ View on Github →

2024-03-02 00:03

Mathlib/Data/Ordmap/Ordset.lean

refactor: optimize proofs with omega (#11093) …

Modified Ordnode.Valid'.node4L_lemma₂ View on Github →

2023-06-02 11:07

Mathlib/Data/Ordmap/Ordset.lean

feat: port Data.Ordmap.Ordset (#4541)

Added Ordnode.Valid'.node4L_lemma₂ View on Github →