Add opposite lemmas to Data.Sign (#1358)

Author: Taneb

CHANGELOG.md

@@ -250,6 +250,12 @@ Other minor additions
   ≤ᵇ-reflects-≤ : Reflects (m ≤ n) (m ≤ᵇ n)
   ```
 
+* Added new proofs in `Data.Sign.Properties`:
+  ```agda
+  s*opposite[s]≡- : ∀ s → s * opposite s ≡ -
+  opposite[s]*s≡- : ∀ s → opposite s * s ≡ -
+  ```
+
 * Added new proof in `Relation.Nullary.Reflects`:
   ```agda
   fromEquivalence : (T b → P) → (P → T b) → Reflects P b

src/Data/Sign/Properties.agda

@@ -129,6 +129,14 @@ s*s≡+ : ∀ s → s * s ≡ +
 s*s≡+ + = refl
 s*s≡+ - = refl
 
+s*opposite[s]≡- : ∀ s → s * opposite s ≡ -
+s*opposite[s]≡- + = refl
+s*opposite[s]≡- - = refl
+
+opposite[s]*s≡- : ∀ s → opposite s * s ≡ -
+opposite[s]*s≡- + = refl
+opposite[s]*s≡- - = refl
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------