proposition: Lemma product_inv_M:forall mu, mu = (product MM (product inv_MM mu)).
proof: Proof. intro mu; rewrite product_associative; replace inv_MM with (inv_digit MM); trivial; rewrite product_digit_inv_digit_identity_right; rewrite product_idM_identity_left; reflexivity. Qed.
imports: Streams Streams_addenda Raxioms