proposition: Lemma succ_is_plus_1 alpha : alpha + 1 = succ alpha.
proof: Proof. unfold succ ; cbn; destruct alpha; cbn; destruct n, n0; try f_equal; abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)