IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic

declarations in this module (21)

• def add L30
• theorem add_def L36
• theorem add_zero_eq L39
• theorem add_succ_eq L42
• theorem zero_add_eq L45
• theorem succ_add_eq L53
• theorem add_comm L61
• theorem add_assoc L69
• theorem toNat_add L80
• theorem toNat_inj L92
• theorem add_left_cancel L100
• theorem add_right_cancel L108
• def mul L117
• theorem mul_def L123
• theorem mul_zero_eq L126
• theorem mul_succ_eq L129
• theorem zero_mul_eq L132
• theorem succ_mul_eq L140
• theorem mul_comm L151
• theorem toNat_mul L160
• theorem mul_ne_zero L172