proposition: Lemma product_digit_inv_digit_identity_right:forall (d:Digit), product d (inv_digit d) = idM.
proof: Proof. intros [ | | ]; unfold map_digits, inv_digit, inv_LL, inv_RR, inv_MM, idM, product, fst, snd; apply (f_equal2 (@pair Vector Vector)); apply (f_equal2 (@pair Q Q)); qZ_numerals. Qed.
imports: Streams Streams_addenda Raxioms