proposition: Lemma product_init_zip_S:forall xi alpha beta n, product_init_zip xi alpha beta (S n) = right_product (left_product (product_init_zip xi alpha beta n) (Str_nth n alpha)) (Str_nth n beta).
proof: Proof. intros xi alpha beta [|n]; trivial. Qed.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)