Metamath Proof Explorer

Table of Contents - 20.34.4. N-Digit Addition Proof Generator

This section formalizes theorems used in an n-digit addition proof generator.

Other theorems required: deccladdcomli00idaddid1iaddid2ieqiddec0hdecadddecaddc.

1. unitadd