add proof for right distributivity of multiplication. tried doing it in a text file first, got the right idea but ran into problems with matching. should check answer -- seems far too long (mostly because of Coq matching problems!)