proposition: Lemma m_product_left_right_product_associative: forall M T N P, m_product M (right_product (left_product T N) P)=right_product (left_product (m_product M T) N) P.
proof: Proof. intros ((A,B),(C,D)) (((a,b),(c,d)),((e,f),(g,h))) ((E,F),(G,H)) ((I,J),(K,L)). unfold m_product, left_product, right_product, fst, snd. apply (f_equal2 (@pair Matrix Matrix)); apply (f_equal2 (@pair Vector Vector)); apply (f_equal2 (@pair Q Q)); ring. Qed.
imports: Streams Streams_addenda Raxioms