Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_compat_from_integer (Lean4Axiomatic/Rational/Impl/Fraction/Negation.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a : ℤ
⊢ from_integer (-a) ≃ -from_integer a
Tactic:
show (-a)//1 ≃ -(a//1)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a : ℤ
⊢ (-a)//1 ≃ -a//1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a : ℤ
⊢ (-a)//1 ≃ -a//1
Tactic:
exact eqv_refl
State after:
no goals