proposition: Lemma product_left_right_product_associative: forall T M1 M2 N1 N2, right_product (left_product (right_product (left_product T M1) N1) M2) N2= right_product (left_product T (product M1 M2)) (product N1 N2).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A1,B1),(C1,D1)) ((A2,B2),(C2,D2)) ((E1,F1),(G1,H1)) ((E2,F2),(G2,H2)); unfold 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