proposition: Lemma succb_correct (alpha: t) : succb alpha <-> exists beta: t, alpha = succ beta.
proof: Proof. destruct alpha; split. - destruct n. + intro; discriminate. + exists n; reflexivity. - intros [[p| p] H]. + injection H; intro; subst; reflexivity. + discriminate. - destruct n. + intro; discriminate. + exists (inr n); reflexivity. - intros [[p| p] H]. + discriminate. + injection H; intro; subst; reflexivity. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)