theorem-proving - リーンを使用して代数式で括弧を削除する方法

Question

リーンを使用して 1 つの代数定理を証明しようとしています。私のコードは

 import algebra.group
import algebra.ring
open algebra

variable {A : Type}

variables [s : ring A] (a b c : A)
include s

theorem clown (a b c d e : A) : 
(a + b  + e) * ( c + d) =   a * c + (b * c + e* c) + (a * d + b * d + e * d)   :=
calc

(a + b  + e) * ( c + d) = (a + (b + e))* (c +d)   : !add.assoc
                    ... = (a + (b + e)) * c + (a + (b + e)) * d   : by rewrite  left_distrib
                    ... =  a * c + (b + e) * c + (a + ( b + e)) * d : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a + (b + e)) * d : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a * d + (b + e) * d) : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a * d + (b * d + e * d) ) : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a * d + b * d + e * d ) :  !add.assoc

 check clown

最後の括弧を削除する方法を教えてください。つまり、手に入れたいだけ

a * c + b * c + e* c + a * d + b * d + e * d

どうもありがとう。