Prove saturation

algebraic-graphs · Apr 16, 2017 · 82a71e8 · 82a71e8
1 parent 69b2b13
commit 82a71e8
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/Theorems.agda b/src/Theorems.agda
@@ -33,6 +33,15 @@ open import Reasoning A
 +idempotence : ∀ {x} -> x + x ≡ x
 +idempotence = transitivity (symmetry +identity) +pre-idempotence
 
+saturation : ∀ {x} -> x * x * x ≡ x * x
+saturation {x} =
+  begin
+    (x * x) * x             ≡⟨ decomposition  ⟩
+    (x * x + x * x) + x * x ≡⟨ L +idempotence ⟩
+    x * x + x * x           ≡⟨ +idempotence   ⟩
+    x * x
+  ∎
+
 absorption : ∀ {x y} -> x * y + x + y ≡ x * y
 absorption {x} {y} =
   begin