Simple theorems like in 2 number addition the carry out is always 0 or 1 are just right for K-6. This theorem can be done informally in examples, then proven informally, and then proven formally by mathematical induction. The latter can use Green Induction (TM).
The machinery to prove this is covered already in my book on Peano Axioms.
A new book forthcoming on place value addition in the Peano Axiom framework will cover the proof of the above two number addition carry out bounded theorem.
We need to name these obvious relationships, call them theorems and prove them. Then k-6 students can learn proofs. These may seem to trivial to prove, but that just proves they are the right difficulty for learning proofs in K-6.
This will turn K-6 into math thinking. This will really teach concepts.
The mistake in New Math was not to focus on the place value algorithms as the place to teach how to prove easy theorems.
Proving theorems is exciting. Taking out this excitement disables the inspiration part of math class. That leaves drill. It also removes the key step in teaching concepts, which is teaching proofs.
The proofs need to be about the core algorithms we teach, the place value algorithms.