proposition: Lemma product_init_zip_folds:forall xi alpha beta n, product_init_zip xi alpha beta (S n) = product_init_zip (right_product (left_product xi (Streams.hd alpha)) (Streams.hd beta)) (Streams.tl alpha) (Streams.tl beta) n.
proof: Proof. intros xi alpha beta n; generalize xi alpha beta; clear xi alpha beta; induction n; intros xi alpha beta; simpl; trivial; rewrite <- IHn; rewrite product_init_zip_S; apply (f_equal2 right_product); trivial. Defined.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)