module NotStructurallyRecursive.Lemmas where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
import Data.Nat.Properties as Nat
open Nat.SemiringSolver
lemma₁ : forall {s} n₁ n₂ n₃ ->
1 + s ≡ 3 + n₁ + n₂ + n₃ -> s ≡ n₁ + (2 + n₂ + n₃)
lemma₁ n₁ n₂ n₃ refl =
solve 3 (λ n₁ n₂ n₃ →
con 2 :+ n₁ :+ n₂ :+ n₃ := n₁ :+ (con 2 :+ n₂ :+ n₃))
refl n₁ n₂ n₃
lemma₂ : forall {s} n₁ n₂ ->
1 + s ≡ 2 + n₁ + n₂ -> s ≡ n₁ + suc n₂
lemma₂ n₁ n₂ refl =
solve 2 (λ n₁ n₂ → con 1 :+ (n₁ :+ n₂) := n₁ :+ (con 1 :+ n₂))
refl n₁ n₂