proposition: Lemma modulus_h_L:forall (mu:Matrix) (alpha:Reals) (t: emits_h mu alpha),(Incl_M mu LL) -> modulus_h mu alpha t = pairT LL (pairT (product inv_LL mu) alpha).
proof: Proof. intros mu alpha t t_l. transitivity (modulus_h mu alpha (emits_h_L _ _ t_l)). apply modulus_h_PI. simpl; case (Incl_M_dec_D mu LL); try contradiction; intros; reflexivity. Defined.
imports: digits