open import Paths
open import Logic::False
open import Arith::Nat::Core

def *-suc-suc (m n : Nat) : suc (m + n + m * n) = suc m * suc n
  ⇒ pmap suc (<=3=> (pmap (+ m * n) +-comm)
    +-assoc (pmap (n +) *-suc))

def z≠s {a : Nat} (p : 0 = suc a) : False ⇒ coe 0 1 (\i ⇒ diag (p i)) a
private def diag Nat : Type
| 0 ⇒ Nat
| suc a ⇒ False

private def suc-inj (m : Nat) : Nat
| 0 ⇒ 114514
| suc m ⇒ m
def s=s {m n : Nat} (p : suc m = suc n) : m = n ⇒ (\ i ⇒ suc-inj (p i))