proposition: Lemma product_init_folds:forall mu alpha n, (product_init mu alpha (S n) = (product_init (product mu (Streams.hd alpha)) (Streams.tl alpha) n)).
proof: Proof. intros mu alpha n; generalize mu alpha; clear mu alpha; induction n; intros mu alpha; simpl; trivial; rewrite <- IHn; rewrite product_init_S; apply (f_equal2 product); trivial. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep