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