intro (c₁——c₂)
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ ∀ {c : Difference ℕ}, a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c₁——c₂ → a₁——a₂ ≃ c₁——c₂