proposition: Lemma modulus_h_absorbs:forall (mu:Matrix) (alpha:Reals) (t: emits_h mu alpha),~(Incl_M mu LL)->~(Incl_M mu RR)->~(Incl_M mu MM)-> forall t', modulus_h mu alpha t = modulus_h (product mu (hd alpha)) (tl alpha) t'.
proof: Proof. intros mu alpha t t_l t_r t_m t'. transitivity (modulus_h mu alpha (emits_h_absorbs _ _ t')). apply modulus_h_PI. simpl. case (Incl_M_dec_D mu LL); try contradiction; case (Incl_M_dec_D mu RR); try contradiction; case (Incl_M_dec_D mu MM); try contradiction; intros _; reflexivity. Defined.
imports: digits