proposition: Lemma m_ge : m big_h <= m small_h.
proof: Proof. unfold small_h; generalize (m big_h) as i. induction i. - auto with arith. - apply Nat.le_lt_trans with (m (iota i)). + assumption. + apply (variant_decr 0). * discriminate. * cbn; apply round_S; exact 0. Qed.
imports: Coq(Arith Lia) hydras(Hydra_Lemmas ON_Generic ON_Omega)