proposition: Lemma m_product_inv_M: forall xi, xi = m_product MM (m_product inv_MM xi).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))); unfold map_digits, inv_digit, inv_MM, m_product, fst, snd; apply (f_equal2 (@pair Matrix Matrix)); apply (f_equal2 (@pair Vector Vector)); apply (f_equal2 (@pair Q Q)); qZ_numerals; field ;auto. Qed.
imports: Streams Streams_addenda Raxioms