proposition: Lemma Successor_inv3 : forall i j, ~ Successor (inr j) (inl i).
proof: Proof. destruct 1 as [H H0]. specialize (H0 (inl (S i))). assert (H1: inl i o< inl (S i)) by (constructor;auto). assert (H2: inl (S i) o< inr j) by constructor. specialize (H0 H1 H2); inversion H0. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)