proposition: Lemma depth_h_Incl_M_inf : forall mu alpha (t: emits_h mu alpha) n, depth_h mu alpha t = n -> {Incl_M (product_init mu alpha n) LL}+{Incl_M (product_init mu alpha n) RR}+{Incl_M (product_init mu alpha n) 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). left; left; trivial. case (Incl_M_dec_D mu RR). left; right; trivial. case (Incl_M_dec_D mu MM). right; trivial... intros t_m t_r t_l; 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. decompose sum (IHn _ _ _ (eq_add_S _ _ H_eq)); [ left; left | left; right | right ]; trivial. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep