proposition: Lemma m_ge : m big_h o<= m small_h.
proof: Proof. unfold small_h; pattern (m big_h); apply well_founded_induction with (R := ON_lt) (1:= ON_wf); intros (i,j) IHij. destruct j as [|k]. - destruct i as [| l]. + apply le_0. + assert (is_true (limitb (S l, 0))) by reflexivity. specialize (limit_is_lub (S l, 0) H (m (iota (S l, 0)))). intros <- k; eapply Comparable.le_lt_trans. apply IHij;left; auto. red; apply (m_strict_mono m Hvar); auto with hydra. simpl canon. apply step_to_battle. apply limit_step. - change (i, S k) with (succ (i,k)) at 1. rewrite <- (lt_succ_le (i,k) (m (iota (i, S k)))). eapply (Comparable.le_lt_trans). instantiate (1:= (m (iota (i, k)))). apply IHij; right; auto. apply (m_strict_mono m Hvar); auto with hydra. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)