proposition: Lemma product_init_zip_init_rev_id: forall xi alpha beta n, xi = (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n)).
proof: Proof. intros xi alpha beta n; generalize xi alpha beta; clear xi alpha beta; induction n; intros xi alpha beta. unfold product_init_zip, product_init_rev; simpl; rewrite right_left_product_idM_identity_right; reflexivity. unfold product_init_rev; repeat rewrite rev_take_S_Str_nth; repeat rewrite fold_right_cons; replace (fold_right product idM (rev (take n (Streams.map inv_digit alpha)))) with (product_init_rev alpha n); trivial; replace (fold_right product idM (rev (take n (Streams.map inv_digit beta)))) with (product_init_rev beta n); trivial; repeat rewrite <- Str_nth_map_pointwise; rewrite product_init_zip_S; rewrite product_left_right_product_associative; rewrite (product_associative (map_digits (Str_nth n alpha))); rewrite product_digit_inv_digit_identity_right; rewrite (product_associative (map_digits (Str_nth n beta))); rewrite product_digit_inv_digit_identity_right; rewrite <- product_left_right_product_associative; rewrite right_left_product_idM_identity_right; apply IHn. Qed.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)