proposition: Lemma product_init_S:forall mu alpha n, product_init mu alpha (S n) = product (product_init mu alpha n) (Str_nth n alpha).
proof: Proof. intros mu alpha [|n]; trivial. Qed.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep