proposition: Lemma m_decrease : forall j h0 i h, h <> head -> rounds standard i h j h0 -> m h0 t1< m h.
proof: Proof. induction 2. - apply Lvar with i; auto. - destruct (h_eq_dec h'' head). + rewrite e in H1; assert False by (eapply standard_battle_head; eauto); contradiction. + apply LT_trans with (m h'');auto. apply Lvar with i; auto. Qed.
imports: hydras(Epsilon0_Needed_Generic)