proposition: Lemma depth_q_Incl_T_inf_strong_general : forall (xi : Tensor) (alpha beta: Reals) (t : emits_q xi alpha beta) (n : nat), depth_q xi alpha beta t = n -> exists d,Incl_T (product_init_zip xi alpha beta n) d /\ fst (modulus_q xi alpha beta t) = d.
proof: Proof. intros xi alpha beta t n H_depth. destruct (depth_q_Incl_T_inf_strong _ _ _ t n H_depth) as [[Hd|Hd]|Hd]; [ exists LL | exists RR | exists MM ]; assumption. Qed.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)