∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumSq a → Prop} {a : R}
  (t : IsSumSq a), motive 0 ⋯ → (∀ (a : R) {s : R} (hs : IsSumSq s), motive (a * a + s) ⋯) → motive a t