proposition: Lemma Successor_inv2 : forall i j, Successor (inr j) (inr 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. exfalso. specialize (H0 (inr (S i))). assert (H2 :inr i o< inr (S i)) by (constructor; auto). assert (H3 :inr (S i) o< inr j) by (constructor; auto). apply (H0 H2 H3). Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)