Prove that join is monotonic in both arguments

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice.agda

@@ -62,6 +62,26 @@ record IsSemilattice {a} (A : Set a)
                     (a ⊔ a₁) ⊔ (a ⊔ a₂)
                 ∎
 
+    ⊔-Monotonicʳ : ∀ (a₂ : A) → Monotonic _≼_ _≼_ (λ a₁ → a₁ ⊔ a₂)
+    ⊔-Monotonicʳ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong a₁≼a₂ (≈-refl {a}))
+        where
+            lhs =
+                begin
+                    (a₁ ⊔ a₂) ⊔ a
+                ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-idemp _)) ⟩
+                    (a₁ ⊔ a₂) ⊔ (a ⊔ a)
+                ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
+                    ((a₁ ⊔ a₂) ⊔ a) ⊔ a
+                ∼⟨ ≈-⊔-cong (⊔-assoc _ _ _) ≈-refl ⟩
+                    (a₁ ⊔ (a₂ ⊔ a)) ⊔ a
+                ∼⟨ ≈-⊔-cong (≈-⊔-cong ≈-refl (⊔-comm _ _)) ≈-refl ⟩
+                    (a₁ ⊔ (a ⊔ a₂)) ⊔ a
+                ∼⟨ ≈-⊔-cong (≈-sym (⊔-assoc _ _ _)) ≈-refl ⟩
+                    ((a₁ ⊔ a) ⊔ a₂) ⊔ a
+                ∼⟨ ⊔-assoc _ _ _ ⟩
+                    (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
+                ∎
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a