def Eq1117.op (a b : ℤ) : ℤ

Equations

• Eq1117.op a b = 2 * a - b / 2

theorem Equation1117_not_implies_Equation2441 : ∃ (G : Type) (x : Magma G), Equation1117 G ∧ ¬Equation2441 G