proposition: Lemma m_lt : m small_h t1< m big_h.
proof: Proof. destruct Rem4 as [x [i H]]. eapply m_decrease with i x; eauto. intro H0; unfold big_h in *. clear H; destruct (T1_eq_dec mu T1.zero). - now apply (mu_positive _ mu Hmu m Var Hy). - apply n; destruct mu. + auto. + discriminate H0. Qed.
imports: hydras(Epsilon0_Needed_Generic)