Add small lemma relating ∷ʳ and ++ (#1713)

Author: iblech

CHANGELOG.md

@@ -1029,6 +1029,7 @@ Other minor changes
 * Add new proofs in `Data.List.Properties`:
   ```agda
   ∈⇒∣product : n ∈ ns → n ∣ product ns
+  ∷ʳ-++ : xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
   ```
 
 * Added new definitions and proofs to `Data.Nat.Primality`:

notes/style-guide.md

@@ -261,7 +261,7 @@ line of code, indented by two spaces.
 * Instead, private blocks should only be used to prevent temporary terms and
   records that are defined for convenience from being exported by the module.
 
-* The mutual block is considered obselete. Please use the standard approach
+* The mutual block is considered obsolete. Please use the standard approach
   of placing the type signatures of the mutually recursive functions before
   their definitions.
 

src/Data/List/Properties.agda

@@ -993,6 +993,8 @@ module _ {x y : A} where
   ∷ʳ-injectiveʳ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
   ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)
 
+∷ʳ-++ : ∀ (xs : List A) (a : A) (ys : List A) → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
+∷ʳ-++ xs a ys = ++-assoc xs [ a ] ys
 
 ------------------------------------------------------------------------
 -- DEPRECATED