proposition: Lemma product_init_product_init_pure:forall mu alpha n, product_init mu alpha n = product mu (product_init_pure alpha n).
proof: Proof. intros mu alpha n; revert mu alpha; induction n; intros mu alpha; unfold product_init_pure. simpl; rewrite product_idM_identity_right; trivial. rewrite Streams_addenda.take_S_n; rewrite (Streams_addenda.fold_right_cons product); rewrite product_associative; rewrite product_init_folds; rewrite (IHn (product mu (Streams.hd alpha)) (Streams.tl alpha)); trivial. Qed.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep