proposition: Lemma succ_correct alpha beta : Successor beta alpha <-> beta = succ alpha.
proof: Proof. split. - destruct alpha, beta; intro H. apply Successor_inv1 in H; now subst. destruct (Successor_inv3 _ _ H). destruct (Successor_inv4 _ _ H). apply Successor_inv2 in H; now subst. - intro;subst; now apply Successor_succ. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)