∀ (x : Int.Linear.Var) (k : ℤ) (y : Int.Linear.Var) (p : Int.Linear.Poly),
  Int.Linear.of_var_eq_mul_cert x k y p =
    p.beq' (Int.Linear.Poly.add 1 x (Int.Linear.Poly.add (-k) y (Int.Linear.Poly.num 0)))