proposition: Lemma depth_h_Incl_M_inf_strong_general : forall (mu : Matrix) (alpha : Reals) (t : emits_h mu alpha) (n : nat), depth_h mu alpha t = n -> exists d,Incl_M (product_init mu alpha n) d /\ fst (modulus_h mu alpha t) = d.
proof: Proof. intros mu alpha t n H_depth. destruct (depth_h_Incl_M_inf_strong _ _ t n H_depth) as [[Hd|Hd]|Hd]; [ exists LL | exists RR | exists MM ]; assumption. Qed.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep