The Coq mailing list

[coqcdp <coqcdpnxj AT 163.com>]

Hi,

      Recently I want to prove associativity law in algebra ,I have proved that with 3 parameters,but I don't know how to prove that with arbitrary n parameters. for example I can prove  (a+b)+c = a +(b+c)  with coq , but  I don't know how to prove  or  formalize (a1+a2)+...+an=a1+(a2+a3)+...+an=...=a1+a2+...+(an-1+an). I hope you can give me some suggestions. Thank you .

    

        Yours Sincerely ,

                                   D.P.Chen