∀ {R : Type u_1} [inst : CommRing R] [inst_1 : ValuativeRel R] (n : ℕ) (t : ValuativeRel.ValueGroupWithZero R),
  ValuativeRel.ValueGroupWithZero.lift (fun a b => ValuativeRel.ValueGroupWithZero.mk (a ^ (n + 1)) (b ^ (n + 1))) ⋯ t =
    ValuativeRel.ValueGroupWithZero.lift (fun a b => ValuativeRel.ValueGroupWithZero.mk (a ^ n) (b ^ n)) ⋯ t * t