Fixed deprecation warnings in Data.Bin.Properties

src/Data/Bin/Properties.agda

@@ -77,7 +77,7 @@ as 1# ≟ bs 1# with as ≟ₑ bs
   1+ (m₁ +ℕ n₁ *ℕ 2) ≤⟨ s≤s (ℕₚ.+-monoˡ-≤ _ (𝔽ₚ.toℕ≤pred[n] a)) ⟩
   1+ (1 +ℕ n₁ *ℕ 2)  ≡⟨ refl ⟩
   1+ n₁ *ℕ 2         ≤⟨ ℕₚ.*-mono-≤ lt ℕₚ.≤-refl ⟩
-  n₂ *ℕ 2            ≤⟨ ℕₚ.n≤m+n m₂ (n₂ *ℕ 2) ⟩
+  n₂ *ℕ 2            ≤⟨ ℕₚ.m≤n+m (n₂ *ℕ 2) m₂ ⟩
   m₂ +ℕ n₂ *ℕ 2      ∎)
   where
   open ℕₚ.≤-Reasoning
@@ -94,7 +94,7 @@ as 1# ≟ bs 1# with as ≟ₑ bs
   m₁ = Fin.toℕ a; m₂ = Fin.toℕ b; n = toℕ (bs 1#)
 
 1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1#
-1<[23] {b} = less (ℕₚ.n≤m+n (Fin.toℕ b) 2)
+1<[23] {b} = less (ℕₚ.m≤n+m 2 (Fin.toℕ b))
 
 1<2+ : ∀ {b bs} → [] 1# < (b ∷ bs) 1#
 1<2+ {_} {[]}     = 1<[23]