proposition: Lemma product_init_pure_ub:forall alpha n, as_Moebius_Q (product_init_pure alpha n) Qone = ub alpha n.
proof: Proof. intros alpha n; revert alpha; induction n; intros [d alpha]; unfold product_init_pure. simpl; auto. rewrite ub_S_n. rewrite Streams_addenda.take_S_n; rewrite (Streams_addenda.fold_right_cons product). unfold map_reals. rewrite Streams_addenda.map_spelled. unfold hd, tl. fold map_reals. rewrite <- (IHn alpha). replace (List.fold_right product idM (Streams_addenda.take n (map_reals alpha))) with (product_init_pure alpha n); trivial. rewrite as_Moebius_Q_product; trivial. apply Is_refining_M_denom_nonvanishing_M. apply Is_refining_M_product_init_pure. realify_Q; apply one_is_in_base_interval. rewrite (IHn alpha); qZ_numerals; apply ub_is_in_base_interval_low. rewrite (IHn alpha); qZ_numerals; apply ub_is_in_base_interval_up. destruct d; [apply Is_refining_M_L|apply Is_refining_M_R|apply Is_refining_M_M]. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M