proposition: Lemma depth_q_modulus_q:forall (xi:Tensor) (alpha beta:Reals) (t: emits_q xi alpha beta) n,depth_q xi alpha beta t=n-> exists d:Digit, modulus_q xi alpha beta t = pairT d (pairT (m_product (inv_digit d) (product_init_zip xi alpha beta n)) (pairT (drop n alpha) (drop n beta))).
proof: Proof. intros xi alpha beta t n H_eq. generalize xi alpha beta t H_eq; clear xi alpha beta t H_eq; induction n; intros xi alpha beta t H_eq. simpl. case (Incl_T_dec_D xi LL); intro t_l. exists LL; rewrite (modulus_q_L _ _ _ t t_l); trivial. case (Incl_T_dec_D xi RR); intro t_r. exists RR; rewrite (modulus_q_R _ _ _ t t_l t_r); trivial. case (Incl_T_dec_D xi MM); intro t_m. exists MM; rewrite (modulus_q_M _ _ _ t t_l t_r t_m); trivial. apply False_ind; rewrite (depth_q_absorbs xi alpha beta t t_l t_r t_m (emits_q_absorbs_inv xi alpha beta t_l t_r t_m t)) in H_eq; discriminate. case (Incl_T_dec_D xi LL); intro t_l. apply False_ind; rewrite (depth_q_L xi alpha beta t t_l) in H_eq; discriminate. case (Incl_T_dec_D xi RR); intro t_r. apply False_ind; rewrite (depth_q_R xi alpha beta t t_l t_r) in H_eq; discriminate. case (Incl_T_dec_D xi MM); intro t_m. apply False_ind; rewrite (depth_q_M xi alpha beta t t_l t_r t_m) in H_eq; discriminate. rewrite (depth_q_absorbs xi alpha beta t t_l t_r t_m (emits_q_absorbs_inv xi alpha beta 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_q_absorbs xi alpha beta t t_l t_r t_m (emits_q_absorbs_inv xi alpha beta t_l t_r t_m t)). rewrite H_ind. apply (@f_equal2 _ _ _ (@pairT Digit (@prodT Tensor (@prodT Reals Reals)))); trivial; apply (@f_equal2 _ _ _ (@pairT Tensor (@prodT Reals Reals))); trivial. rewrite product_init_zip_folds; trivial. destruct alpha; destruct beta; reflexivity. Defined.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)