proposition: Lemma Successor_inv1 : forall i j, Successor (inl j) (inl i) -> j = S i.
proof: Proof. destruct 1 as [H H0]. inversion_clear H. assert (H2 : (j = S i \/ S i < j)%nat) by lia. destruct H2; trivial. assert False. { assert (H2: inl i o< inl (S i)) by (constructor; auto). assert (H3: inl (S i) o< inl j) by (constructor; auto). apply (H0 (inl (S i)) H2 H3). } contradiction. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)