[ deprecate ] `Data.Fin.Base.lower₁` in favour of `Data.Fin.Base.lower`

[jamesmckinna]

As a consequence of #2748 , which introduced Data.Fin.Base.lower, #2783 changes the type of lower₁ such that the following lemmas become easily provable (because each function now takes an irrelevant argument), so the heart of each proof is refl.

They justify that lower₁ can be deprecated in favour of lower.

lower₁≗lower : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) →
               lower₁ i n≢i ≡ lower i (ℕ.≤∧≢⇒< (toℕ≤pred[n]′ i) (n≢i ∘ sym))
lower₁≗lower {n = zero}   zero    0≢0 = contradiction-irr refl 0≢0
lower₁≗lower {n = suc _ } zero    _   = refl
lower₁≗lower {n = suc _ } (suc i) ne  = cong suc (lower₁≗lower i (ne ∘ cong suc))

lower≗lower₁ : ∀ (i : Fin (suc n)) .(i<n : toℕ i ℕ.< n) →
               lower i i<n ≡ lower₁ i (ℕ.<⇒≢ i<n ∘ sym)
lower≗lower₁ {n = suc _ } zero    _   = refl
lower≗lower₁ {n = suc _ } (suc i) lt  = cong suc (lower≗lower₁ i (ℕ.s<s⁻¹ lt))

There is only one use of lower₁ in stdlib, in Data.Fin.Induction.>-weakInduction, and as already noted, this can be changed in favour of an appeal to Data.Fin.Relation.Unary.Top to do the inversion of inject₁ directly.

>-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
                  P (fromℕ n) →
                  (∀ i → P (suc i) → P (inject₁ i)) →
                  ∀ i → P i
>-weakInduction P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i)
  where
  induct : ∀ {i} → Acc _>_ i → P i
  induct {i} (acc rec) with Data.Fin.Relation.Unary.Top.view i
  ... | ‵fromℕ = Pₙ
  ... | ‵inject₁ j = Pᵢ₊₁⇒Pᵢ j (induct (rec (s≤s (≤-reflexive (toℕ-inject₁ j)))))