proposition: Lemma Successor_succ alpha : Successor (succ alpha) alpha.
proof: Proof. destruct alpha;red;cbn; split. - constructor; auto. - destruct z as [n0 | n1]. inversion_clear 1. inversion_clear 1; abstract lia. inversion 2. - constructor; auto. - destruct z as [n0 | n1]. inversion_clear 1. inversion_clear 1. inversion_clear 1; abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)