Merge pull request #42 from gl3nnleblanc/main

Two more implications from equation 5
teorth · Sep 28, 2024 · 749679b · 749679b
2 parents 6566506 + 96949da
commit 749679b
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
@@ -91,9 +91,15 @@ theorem Equation4_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4 G) : E
 theorem Equation5_implies_Equation3 (G: Type*) [Magma G] (h: Equation5 G) : Equation3 G :=
   fun _ ↦ h _ _
 
+theorem Equation5_implies_Equation8 (G: Type*) [Magma G] (h: Equation5 G) : Equation8 G :=
+  fun _  ↦ by repeat rw [← h]
+
 theorem Equation5_implies_Equation39 (G: Type*) [Magma G] (h: Equation5 G) : Equation39 G :=
   fun _ _ ↦ by repeat rw [← h]
 
+theorem Equation5_implies_Equation4512 (G: Type*) [Magma G] (h: Equation5 G) : Equation4512 G :=
+  fun _ _ _  ↦ by repeat rw [← h]
+
 theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G :=
   fun a _ ↦ by rw [h a a, ← h]