This might not be the best introduction for someone who hasn't proved "a = b iff a - c = b - c", and e.g. may not be familiar with "if and only if," or the fact that P => Q is considered true if P is false, even if Q is also false.
I have to wonder if highschool math would make more sense to some students if (a) and (b) were taught together.
I might even cut polynomials entirely to make room for the new stuff and do informal calculus earlier.
Math is ultimately about bridging the gap between fuzzy warm intuition and and cold artificial rigor. Focusing on either in isolation defeats the purpose.
For anyone that struggled with pure math because memorizing seemed less "big brained" than informal proofs, computers making thing concrete let alone gamified can help immensely.
It's a good thing then that this framing is rather unlike the intuitionistic mathematics actually suggested.