have elem1 : 3 + 3 = 6 := by norm_num;
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }