proposition: Lemma denom_nonvanishing_product_init: forall (alpha : Reals) (r : R) (n : nat), rep alpha r -> denom_nonvanishing_M (product_init_rev alpha n) r.
proof: Proof. intros alpha r n H_rep. decompose record (product_init_rev_rep_drop_denom_nonvanishing alpha n r (Streams.hd (drop n alpha)) H_rep (refl_equal _)); trivial. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs