proposition: Lemma product_associative:forall M N P, product M (product N P) = product (product M N) P.
proof: Proof. intros ((a0,b0),(c0,d0)) ((a1,b1),(c1,d1)) ((a2,b2),(c2,d2)); unfold product, fst, snd; apply (f_equal2 (@pair Vector Vector)); apply (f_equal2 (@pair Q Q)); ring; auto. Qed.
imports: Streams Streams_addenda Raxioms