proposition: Lemma mu_positive : mu <> T1.zero.
proof: Proof. intro H; subst; specialize (m_bounded (hyd1 head)). intro H0; destruct (not_LT_zero H0). Qed.
imports: hydras(Hydra_Lemmas Epsilon0 Canon Paths O2H) Coq(Relation_Operators)