diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal')
| -rw-r--r-- | src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda index e186c71..5cf2d5b 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda @@ -202,14 +202,14 @@ x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x⁻¹ x<y⇒ε<y∙x⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹ x<y⇒ε<y∙x⁻¹ {x} {y} x<y = begin-strict ε ≈˘⟨ inverseʳ x ⟩ - x ∙ x ⁻¹ <⟨ ∙-invariantʳ (x ⁻¹) x<y ⟩ + x ∙ x ⁻¹ <⟨ ∙-monoʳ-< x<y ⟩ y ∙ x ⁻¹ ∎ ε<y∙x⁻¹⇒x<y : ∀ {x y} → ε < y ∙ x ⁻¹ → x < y ε<y∙x⁻¹⇒x<y {x} {y} ε<yx⁻¹ = begin-strict x ≈˘⟨ identityˡ x ⟩ - ε ∙ x <⟨ ∙-invariantʳ x ε<yx⁻¹ ⟩ - y ∙ x ⁻¹ ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩ - y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ - y ∙ ε ≈⟨ identityʳ y ⟩ + ε ∙ x <⟨ ∙-monoʳ-< ε<yx⁻¹ ⟩ + y ∙ x ⁻¹ ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩ + y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ + y ∙ ε ≈⟨ identityʳ y ⟩ y ∎ |