proposition: Lemma depth_h_Incl_M_inf_strong : forall mu alpha (t: emits_h mu alpha) n, depth_h mu alpha t = n -> {Incl_M (product_init mu alpha n) LL/\ fst (modulus_h mu alpha t)=LL}+ {Incl_M (product_init mu alpha n) RR/\ fst (modulus_h mu alpha t)=RR}+ {Incl_M (product_init mu alpha n) MM/\ fst (modulus_h mu alpha t)=MM}.
proof: Proof. intros mu alpha t n H_eq. generalize mu alpha t H_eq. clear mu alpha t H_eq. induction n; intros mu alpha t H_eq. case (Incl_M_dec_D mu LL); intro t_l. left; left; split; trivial; rewrite (modulus_h_L _ _ t t_l); trivial. case (Incl_M_dec_D mu RR); intro t_r. left; right; split; trivial; rewrite (modulus_h_R _ _ t t_l t_r); trivial. case (Incl_M_dec_D mu MM); intro t_m. right; split; trivial; rewrite (modulus_h_M _ _ t t_l t_r t_m); trivial... apply False_rec; rewrite (depth_h_absorbs mu alpha t t_l t_r t_m (emits_h_absorbs_inv mu alpha t_l t_r t_m t)) in H_eq; discriminate... case (Incl_M_dec_D mu LL); intro t_l. apply False_rec; rewrite (depth_h_L mu alpha t t_l) in H_eq; discriminate. case (Incl_M_dec_D mu RR); intro t_r. apply False_rec; rewrite (depth_h_R mu alpha t t_l t_r) in H_eq; discriminate. case (Incl_M_dec_D mu MM); intro t_m. apply False_rec; rewrite (depth_h_M mu alpha t t_l t_r t_m) in H_eq; discriminate. rewrite (depth_h_absorbs mu alpha t t_l t_r t_m (emits_h_absorbs_inv mu alpha t_l t_r t_m t)) in H_eq. rewrite product_init_folds. destruct (IHn _ _ _ (eq_add_S _ _ H_eq)) as [[[H_Incl H_modulus]|[H_Incl H_modulus]]|[H_Incl H_modulus]]; [ left; left | left; right | right ]; split; trivial; rewrite <- H_modulus; apply (@f_equal _ _ (@fst Digit (Matrix*Reals))); rewrite (modulus_h_absorbs _ _ t t_l t_r t_m (emits_h_absorbs_inv mu alpha t_l t_r t_m t)); trivial. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep