proposition: Lemma depth_q_L:forall (xi:Tensor) (alpha beta:Reals) (t: emits_q xi alpha beta),(Incl_T xi LL) -> depth_q xi alpha beta t=0.
proof: Proof. intros xi alpha beta t t_l. transitivity (depth_q xi alpha beta (emits_q_L _ _ _ t_l)). apply depth_q_PI. simpl; case (Incl_T_dec_D xi LL); try contradiction; intros; reflexivity. Defined.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)