proposition: Lemma Q_to_R_as_Moebius:forall mu q, denom_nonvanishing_M mu (Q_to_R.Q_to_R q)-> Q_to_R.Q_to_R (as_Moebius_Q mu q) = as_Moebius mu (Q_to_R.Q_to_R q).
proof: Proof. intros ((a,b),(c,d)) q; unfold denom_nonvanishing_M, as_Moebius_Q, as_Moebius, fst, snd; intro Hcd; Q_to_R.realify_Q; trivial; apply Q_to_R.Q_to_R_Qneq; Q_to_R.realify_Q; trivial. Qed.
imports: Streams Streams_addenda Raxioms