proposition: Lemma depth_q_Incl_T_inf_strong : forall xi alpha beta (t: emits_q xi alpha beta) n, depth_q xi alpha beta t = n -> {Incl_T (product_init_zip xi alpha beta n) LL/\ fst (modulus_q xi alpha beta t)=LL}+ {Incl_T (product_init_zip xi alpha beta n) RR/\ fst (modulus_q xi alpha beta t)=RR}+ {Incl_T (product_init_zip xi alpha beta n) MM/\ fst (modulus_q xi alpha beta t)=MM}.
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. case (Incl_T_dec_D xi LL); intro t_l. left; left; split; trivial; rewrite (modulus_q_L _ _ _ t t_l); trivial. case (Incl_T_dec_D xi RR); intro t_r. left; right; split; trivial; rewrite (modulus_q_R _ _ _ t t_l t_r); trivial. case (Incl_T_dec_D xi MM); intro t_m. right; split; trivial; rewrite (modulus_q_M _ _ _ t t_l t_r t_m); trivial... apply False_rec; 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_rec; 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_rec; 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_rec; 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. rewrite product_init_zip_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 (Tensor*(Reals*Reals)))); rewrite (modulus_q_absorbs _ _ _ t t_l t_r t_m (emits_q_absorbs_inv xi alpha beta t_l t_r t_m t)); trivial. Defined.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)