proposition: Lemma Is_refining_M_product_init: forall mu alpha n, Is_refining_M mu -> Is_refining_M (product_init mu alpha n).
proof: Proof. intros mu alpha n H_mu; rewrite product_init_product_init_pure; apply Is_refining_M_product; trivial; apply Is_refining_M_product_init_pure. Qed.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep