------------------------------------------------------------------------ -- Some boring lemmas ------------------------------------------------------------------------ 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₂