proposition: Lemma m_ge : m big_h t1<= m small_h.
proof: Proof. unfold big_h, small_h. eapply m_ge_generic; trivial. intros; eapply variant_decr; eauto. intro; subst h; apply (head_no_round_n _ _ H). Qed.
imports: hydras(Epsilon0_Needed_Generic)