BCoPL exercise 1-3 (1)(2)

gistfile1.agda

ex-1-3-1 : ∀ {n₁ n₂ n₃} → (p : n₁ plus n₂ is n₃) → steps-plus p ≡ 1 + n₁
ex-1-3-1 P-Zero = refl
ex-1-3-1 (P-Succ p) = cong S (ex-1-3-1 p)

ex-1-3-2 : ∀ {n₁ n₂ n₃} → (p : n₁ times n₂ is n₃) → steps-times p ≡ 1 + n₁ * (n₂ + 2)
ex-1-3-2 T-Zero = refl
ex-1-3-2 (T-Succ t p) = cong S (plus+times≡n₂+2+n₁[n₂+2] t p)
  where
    S[a+Sb]≡a+2+b : (a b : ℕ) → S (a + S b) ≡ a + 2 + b
    S[a+Sb]≡a+2+b Z b = refl
    S[a+Sb]≡a+2+b (S a) b = cong S (S[a+Sb]≡a+2+b a b)
    plus+times≡n₂+2+n₁[n₂+2] : ∀ {n₁ n₂ n₃ n₄}
                             (t : n₁ times n₂ is n₄) → (p : n₂ plus n₄ is n₃) →
                             steps-plus p + steps-times t ≡ n₂ + 2 + n₁ * (n₂ + 2)
    plus+times≡n₂+2+n₁[n₂+2] {n₁} {n₂} {n₃} {n₄} t p rewrite
      ex-1-3-1 p | ex-1-3-2 t | S[a+Sb]≡a+2+b n₂ (n₁ * (n₂ + 2)) = refl