proposition: Lemma product_idM_identity_left:forall M, product idM M = M.
proof: Proof. intros ((a,b),(c,d)); unfold idM, product, fst, snd, Qdiv at 2 4 5 7; rewrite Qmult_zero; repeat rewrite Qmult_zero_right; repeat rewrite Qplus_zero_right; repeat rewrite Qplus_zero_left; qZ_numerals; rewrite Qdiv_Qone_Qone; repeat rewrite Qmult_one_left; trivial. Qed.
imports: Streams Streams_addenda Raxioms