proposition: Lemma as_Moebius_Q_L_nondecreasing:forall x y, (Qopp Qone) <= x -> y<= Qone -> x<=y -> as_Moebius_Q LL x <= as_Moebius_Q LL y.
proof: Proof. intros x y Hx Hy Hxy. unfold as_Moebius_Q, map_digits, fst, snd. assert (H_x_one_nonneg: Zero <= x+1). stepr (x-(Qopp 1)); try ring; apply Qle_Qminus_Zero; auto. assert (H_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 * x * 2 + 3 * 2). stepr (2*(x+3)); [|qZ_numerals; ring]. apply Qlt_mult_pos_pos; auto. assert (H_y_one_nonneg: Zero <= y+1). stepr (y-(Qopp 1)); try ring; apply Qle_Qminus_Zero; auto; apply Qle_trans with x; auto. assert (H_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 * y * 2 + 3 * 2). stepr (2*(y+3)); [|qZ_numerals; 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; [|qZ_numerals; ring]. apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero; auto. Qed.
imports: Streams Streams_addenda Raxioms