proposition: Lemma product_init_zip_product_init_pure:forall xi alpha beta n, product_init_zip xi alpha beta n = right_product (left_product xi (product_init_pure alpha n)) (product_init_pure beta n).
proof: Proof. intros xi alpha beta n; revert xi alpha beta; induction n; intros xi alpha beta; unfold product_init_pure. simpl; rewrite right_left_product_idM_identity_right; trivial. repeat rewrite Streams_addenda.take_S_n; repeat rewrite (Streams_addenda.fold_right_cons product); rewrite <- product_left_right_product_associative; rewrite product_init_zip_folds; rewrite (IHn (right_product (left_product xi (Streams.hd alpha)) (Streams.hd beta)) (Streams.tl alpha) (Streams.tl beta)); trivial. Qed.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)