add2mul Show Code edit
## Adding twice mean Multiply by 2
## right('Simplify', '2')
thm (add2mul () () (= (+ A A) (* (2) A))
## <d 'Distributive Property '>
(1) (1) A distl
(= (* (+ (1) (1)) A) (+ (* (1) A) (* (1) A)))
A mulidr
(= (* (1) A) A)
EqReplaceEq1Add0
(= (* (+ (1) (1)) A) (+ A (* (1) A)))
A mulidr
(= (* (1) A) A)
EqReplaceEq1Add1
(= (* (+ (1) (1)) A) (+ A A))
## </d 'Distributive Property '>
## <d 'Evaluate'>
1plus1
(= (+ (1) (1)) (2))
EqReplaceEq0Mul0
(= (* (2) A) (+ A A))
## </d 'Evaluate'>
eqcomi
(= (+ A A) (* (2) A))
)
edit