proposition: Lemma modulus_q_absorbs:forall (xi:Tensor) (alpha beta:Reals) (t: emits_q xi alpha beta),~(Incl_T xi LL)->~(Incl_T xi RR)->~(Incl_T xi MM)-> forall t', modulus_q xi alpha beta t = modulus_q (right_product (left_product xi (hd alpha)) (hd beta)) (tl alpha) (tl beta) t'.
proof: Proof. intros xi alpha beta t t_l t_r t_m t'. transitivity (modulus_q xi alpha beta (emits_q_absorbs _ _ _ t')). apply modulus_q_PI. simpl. case (Incl_T_dec_D xi LL); try contradiction; case (Incl_T_dec_D xi RR); try contradiction; case (Incl_T_dec_D xi MM); try contradiction; intros _; reflexivity. Defined.
imports: digits