Some easy proves

Wow.agda

module Wow where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Binary.Core
open import Function
open import Relation.Nullary

-- lemma₁ : ∀ a b → (suc (a + suc a) ≡ suc (b + suc b)) → (a + a ≡ b + b)
-- lemma₁ a b ev
--   rewrite +-comm a (suc a)
--         | +-comm b (suc b)
--         = lemma₀ (a + a) (b + b) (lemma₀ (suc (a + a)) (suc (b + b)) ev)
--   where
--     lemma₀ : ∀ a b → (suc a ≡ suc b) → (a ≡ b)
--     lemma₀ _ _ refl = refl

-- +-invert : ∀ a b → (a + a ≡ b + b) → a ≡ b
-- +-invert zero zero ev = refl
-- +-invert zero (suc b) ()
-- +-invert (suc a) zero ()
-- +-invert (suc a) (suc b) ev
--   rewrite +-invert a b (lemma₁ a b ev) = refl

lemma₁ : ∀ a b → (suc (a + suc a) ≡ suc (b + suc b)) → (a + a ≡ b + b)
lemma₁ a b
  rewrite +-comm a $ suc a
        | +-comm b $ suc b
        = lemma₀ (a + a) (b + b) ∘ lemma₀ (suc $ a + a) (suc $ b + b)
  where
    lemma₀ : ∀ a b → (suc a ≡ suc b) → (a ≡ b)
    lemma₀ _ _ refl = refl

+-invert : ∀ a b → (a + a ≡ b + b) → a ≡ b
+-invert zero zero ev = refl
+-invert zero (suc b) ()
+-invert (suc a) zero ()
+-invert (suc a) (suc b) ev
  rewrite +-invert a b $ lemma₁ a b ev = refl

util : ∀ {ℓ₀ ℓ₁} {P : ℕ → Set ℓ₀} {Q : Set ℓ₁}
      → (∀ a → P (suc a) → Q) → (∀ a → P a → (a ≢ 0) → Q)
util _ zero _ a = ⊥-elim $ a refl
util f (suc a) c d = f a c