proposition: Lemma Successor_succ : forall alpha, Successor (succ alpha) alpha.
proof: Proof. destruct alpha;red;cbn; split. - right; auto. - destruct z as [n1 n2]; unfold succ; cbn; intros H H0; inversion H0; subst; inversion H; subst; abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)