diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index 20ba11b..d572668 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -78,6 +78,24 @@ plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
 postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
 
+minus : SignLattice → SignLattice → SignLattice
+minus ⊥ᵍ _ = ⊥ᵍ
+minus _ ⊥ᵍ = ⊥ᵍ
+minus ⊤ᵍ _ = ⊤ᵍ
+minus _ ⊤ᵍ = ⊤ᵍ
+minus [ + ]ᵍ [ + ]ᵍ = ⊤ᵍ
+minus [ + ]ᵍ [ - ]ᵍ = [ + ]ᵍ
+minus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
+minus [ - ]ᵍ [ + ]ᵍ = [ - ]ᵍ
+minus [ - ]ᵍ [ - ]ᵍ = ⊤ᵍ
+minus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
+minus [ 0ˢ ]ᵍ [ + ]ᵍ = [ - ]ᵍ
+minus [ 0ˢ ]ᵍ [ - ]ᵍ = [ + ]ᵍ
+minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
+
+postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
+postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
+
 module _ (prog : Program) where
     open Program prog