proposition: Lemma modulus_q_R:forall (xi:Tensor) (alpha beta:Reals) (t: emits_q xi alpha beta), ~(Incl_T xi LL) -> (Incl_T xi RR) -> modulus_q xi alpha beta t=pairT RR (pairT (m_product inv_RR xi) (pairT alpha beta)).
proof: Proof. intros xi alpha beta t t_l t_r. transitivity (modulus_q xi alpha beta (emits_q_R _ _ _ t_r)). apply modulus_q_PI. simpl; case (Incl_T_dec_D xi LL); try contradiction; case (Incl_T_dec_D xi RR); try contradiction; intros; reflexivity. Defined.
imports: digits