proposition: Lemma depth_h_M:forall (mu:Matrix) (alpha:Reals) (t: emits_h mu alpha),~(Incl_M mu LL)->~(Incl_M mu RR)->(Incl_M mu MM)-> depth_h mu alpha t = 0.
proof: Proof. intros mu alpha t t_l t_r t_m. transitivity (depth_h mu alpha (emits_h_M _ _ t_m)). apply depth_h_PI. simpl; case (Incl_M_dec_D mu LL); try contradiction; case (Incl_M_dec_D mu RR); try contradiction; case (Incl_M_dec_D mu MM); try contradiction; intros; reflexivity. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep