proposition: Lemma Successor_inv : forall i j k l : nat, Successor (k, l) (i, j) -> i = k /\ l = S j.
proof: Proof. destruct 1 as [H H0]. assert (H1 : (i< k \/ i=k /\ j <l)%nat) by (inversion_clear H; auto). destruct H1 as [H1 | [H1 H2]]. - destruct (H0 (i, (S j))). constructor 2; auto. constructor 1;auto. - subst; destruct (Compat815.le_lt_or_eq _ _ H2); auto. destruct (H0 (k, S j)); constructor 2; auto. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)