proposition: Theorem Impossible : False.
proof: Proof. destruct (StrictOrder_Irreflexive (R:=ON_lt) (m big_h)); eapply le_lt_trans; [apply m_ge | apply m_lt]. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)