proposition: Lemma product_init_init_rev_id: forall mu alpha n, mu = product (product_init mu alpha n) (product_init_rev alpha n).
proof: Proof. intros mu alpha n; generalize mu alpha; clear mu alpha; induction n; intros mu alpha. unfold product_init, product_init_rev; simpl; rewrite product_idM_identity_right; reflexivity. unfold product_init_rev; rewrite rev_take_S_Str_nth; rewrite fold_right_cons; replace (fold_right product idM (rev (take n (Streams.map inv_digit alpha)))) with (product_init_rev alpha n); trivial; rewrite <- Str_nth_map_pointwise; rewrite product_init_S; rewrite <- product_associative; rewrite (product_associative (map_digits (Str_nth n alpha))); rewrite product_digit_inv_digit_identity_right; rewrite product_associative; rewrite product_idM_identity_right; apply IHn. Qed.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep