proposition: Lemma m_big_h_not_null : m big_h <> zero.
proof: Proof. intro H; pose (h1 := hyd1 (hyd1 head)). assert (first_round : big_h -+-> h1). { left; exists 0; right; left; constructor 1 with (n:=0). split; left. } specialize (m_strict_mono m Hvar first_round). rewrite H; inversion_clear 1; lia. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)