∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x y : WittVector p R) (i j : ℕ),
  (⇑WittVector.verschiebung)^[i] x * (⇑WittVector.verschiebung)^[j] y =
    (⇑WittVector.verschiebung)^[i + j] ((⇑WittVector.frobenius)^[j] x * (⇑WittVector.frobenius)^[i] y)