proposition: Corollary m_lt : m small_h o< m big_h.
proof: Proof. apply m_strict_mono with (1:=Hvar) (2:=big_to_small). Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)