Metamath Proof Explorer

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

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

Other theorems required: deccladdcomli00idaddridiaddlidieqiddec0hdecadddecaddc.

1. unitadd