Proof of sum of 0..n is equal to n*(n+1)/2 in Agda

Sum.agda

open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s; _<_)
open import Data.Nat.Properties using (*-distribˡ-+; *-comm; +-assoc; +-comm)
open import Data.Nat.DivMod using (_/_; m*n/n≡m; +-distrib-/; _%_; %-distribˡ-+; m*n%n≡0)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; cong; sym; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡;  _∎)

module Sum where

sum : ℕ → ℕ
sum 0       = 0
sum (suc n) = suc n + sum n

sumᶜ : ℕ → ℕ
sumᶜ n = suc n * n  / 2

sum≡sumᶜ : ∀ n → sum n ≡ sumᶜ n
sum≡sumᶜ zero    = refl
sum≡sumᶜ (suc n) =
  begin
    sum (suc n)
  ≡⟨⟩
    suc n + sum n
  ≡⟨ cong (suc n +_) (sum≡sumᶜ n) ⟩
    suc n + sumᶜ n
  ≡⟨⟩
    suc n + suc n * n / 2
  ≡⟨ cong (_+ (suc n) * n / 2) (sym (m*n/n≡m (suc n) 2)) ⟩
    suc n * 2 / 2 + suc n * n / 2
  ≡⟨ sym (+-distrib-/ (suc n * 2) (suc n * n) {2} (lemma₃ n)) ⟩
    (suc n * 2 + suc n * n) / 2
  ≡⟨ cong (_/ 2) (sym (*-distribˡ-+ (suc n) 2 n)) ⟩
    suc n * (2 + n) / 2
  ≡⟨ cong (_/ 2) (*-comm (suc n) (2 + n)) ⟩
    (2 + n) * suc n / 2
  ≡⟨⟩
    sumᶜ (suc n)
  ∎
  where
    lemma₁ : ∀ n → n + n ≡ n * 2
    lemma₁ zero    = refl
    lemma₁ (suc n) rewrite +-comm n (suc n) | lemma₁ n = refl
    
    lemma₂ : ∀ n → (suc n) * n % 2 ≡ 0
    lemma₂ zero    = refl
    lemma₂ (suc n) =
      begin
        suc (suc n) * (suc n) % 2
      ≡⟨⟩
        (suc n + (suc n + n * suc n)) % 2
      ≡⟨ cong (_% 2) (sym (+-assoc (suc n) (suc n) (n * suc n))) ⟩
        (suc n + suc n + n * suc n) % 2
      ≡⟨ cong (λ x → (x + n * suc n) % 2) (lemma₁ (suc n)) ⟩
        (suc n * 2 + n * suc n) % 2
      ≡⟨ (%-distribˡ-+ (suc n * 2) (n * suc n) 2) ⟩
        (suc n * 2 % 2 + n * suc n % 2) % 2
      ≡⟨ cong (λ x → (x + n * suc n % 2) % 2) (m*n%n≡0 (suc n) 1) ⟩
        (n * suc n % 2) % 2
      ≡⟨ cong (λ x → x % 2 % 2) (*-comm n (suc n)) ⟩
        (suc n * n % 2) % 2
      ≡⟨ cong (_% 2) (lemma₂ n) ⟩
        0 % 2
      ≡⟨⟩
        0
      ∎

    lemma₃ : ∀ n → suc n * 2 % 2 + suc n * n % 2 < 2
    lemma₃ n rewrite m*n%n≡0 (suc n) 1 | lemma₂ n = s≤s z≤n