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