proposition: Lemma as_Moebius_Q_R_nondecreasing:forall x y, (Qopp Qone) <= x -> y<= Qone -> x<=y -> as_Moebius_Q RR x <= as_Moebius_Q RR y.
proof: Proof. intros x y Hx Hy Hxy. unfold as_Moebius_Q, map_digits, fst, snd. assert (H_min_y_one_nonneg: Zero <= -y+1). stepr (1-y); try ring; apply Qle_Qminus_Zero; auto. assert (H_min_y_three_pos: Zero < -y+3). apply Qle_lt_trans with ((-y)+1); auto. apply Qlt_Zero_Qminus; stepr 2; auto; qZ_numerals; ring. assert (H':Zero < (-1)%Z * y * 2 + 3 * 2). rewrite Z_to_Q_min_one; stepr (2*(-y+3)); [|ring]. apply Qlt_mult_pos_pos; auto. assert (H_min_x_one_nonneg: Zero <= -x+1). stepr (1-x); try ring; apply Qle_Qminus_Zero; auto; apply Qle_trans with y; auto. assert (H_min_x_three_pos: Zero < -x+3). apply Qle_lt_trans with ((-x)+1); auto. apply Qlt_Zero_Qminus; stepr 2; auto; qZ_numerals; ring. assert (H:Zero < (-1)%Z * x * 2 + 3 * 2). rewrite Z_to_Q_min_one; stepr (2*(-x+3)); [|ring]. apply Qlt_mult_pos_pos; auto. 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 (16*(y-x)); qZ_numerals; [|ring]. apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero; auto. Qed.
imports: Streams Streams_addenda Raxioms