∀ (k : ℤ) (v : Int.Linear.Var) (k_1 : ℤ) (v_1 : Int.Linear.Var) (p_2 : Int.Linear.Poly),
  Int.Linear.Poly.insert k v (Int.Linear.Poly.add k_1 v_1 p_2) =
    bif Nat.blt v_1 v then Int.Linear.Poly.add k v (Int.Linear.Poly.add k_1 v_1 p_2)
    else
      bif Nat.beq v v_1 then if (k.add k_1 == 0) = true then p_2 else Int.Linear.Poly.add (k.add k_1) v_1 p_2
      else Int.Linear.Poly.add k_1 v_1 (Int.Linear.Poly.insert k v p_2)