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