Do some cleanup in the Lean backend (#257)

1 files changed, 17 insertions, 0 deletions

diff --git a/backends/lean/Base/Core.lean b/backends/lean/Base/Core.lean
new file mode 100644
index 00000000..89dd199b
--- /dev/null
+++ b/backends/lean/Base/Core.lean
@@ -0,0 +1,17 @@
+
+import Lean
+
+/- This lemma is generally useful. It often happens that (because we
+   make a split on a condition for instance) we have `x ≠ y` in the context
+   and need to simplify `y ≠ x` somewhere. -/
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
+/- This is generally useful, and doing without is actually quite cumbersome.
+
+   Note that the following theorem does not seem to be necessary (we invert `x`
+   and `y` in the conclusion), probably because of `neq_imp`:
+   `¬ x = y → ¬ y == x`
+ -/
+@[simp]
+theorem neq_imp_nbeq [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ x == y := by simp [*]