∀ {R : Type u_2} {M : Type u_1} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  (x : TrivSqZeroExt R M) (n : ℕ),
  ∀ x_1 ∈ List.map (fun i => x.fst ^ (n - i + i) • x.snd) (List.range n.succ), x_1 = x.fst ^ n • x.snd