proposition: Lemma depth_h_modulus_h:forall mu alpha (t: emits_h mu alpha) n, depth_h mu alpha t = n -> exists d:Digit, modulus_h mu alpha t = pairT d (pairT (product (inv_digit d) (product_init mu alpha n)) (drop n alpha)).
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. simpl. case (Incl_M_dec_D mu LL); intro t_l. exists LL; rewrite (modulus_h_L _ _ t t_l); trivial. case (Incl_M_dec_D mu RR); intro t_r. exists RR; rewrite (modulus_h_R _ _ t t_l t_r); trivial. case (Incl_M_dec_D mu MM); intro t_m. exists MM; rewrite (modulus_h_M _ _ t t_l t_r t_m); trivial. apply False_ind; 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_ind; 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_ind; 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_ind; 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. destruct (IHn _ _ _ (eq_add_S _ _ H_eq)) as [d H_ind]; exists d. rewrite (modulus_h_absorbs mu alpha t t_l t_r t_m (emits_h_absorbs_inv mu alpha t_l t_r t_m t)). rewrite H_ind. apply (@f_equal2 _ _ _ (@pairT Digit (@prodT Matrix Reals))); trivial; apply (@f_equal2 _ _ _ (@pairT Matrix Reals)); trivial. rewrite product_init_folds; trivial. destruct alpha; reflexivity. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep