proposition: Lemma as_Moebius_Q_M_nondecreasing:forall x y, (Qopp Qone) <= x -> y<= Qone -> x<=y -> as_Moebius_Q MM x <= as_Moebius_Q MM y.
proof: Proof. intros x y Hx Hy Hxy. unfold as_Moebius_Q, map_digits, fst, snd. repeat rewrite Qdiv_Qmult_numerator_r; auto. repeat rewrite Qplus_Qdiv; auto. repeat rewrite Qdiv_Qdiv_simplify; auto. apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (3*(y-x)); [|qZ_numerals; ring]. apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; auto. Qed.
imports: Streams Streams_addenda Raxioms