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