proposition: Lemma ap_cases alpha : ap alpha -> alpha = 1 \/ alpha = omega.
proof: Proof. destruct (zero_limit_succ_dec alpha) as [[Hzero | Hlim] | Hsucc]. - subst alpha; intro H; assert False by (destruct H as [H _]; auto); contradiction. - destruct alpha; unfold ap. destruct n, n0; try discriminate. intros [_ H1]; destruct n. + now right. + right; specialize (H1 (S n,0) (S n,0)). assert (H2:(S n, 0) o< (S (S n), 0)) by (left; auto). specialize (H1 H2 H2). inversion H1; abstract lia. - intro H; destruct Hsucc as [beta e]; subst. destruct H as [_ H]. destruct (eq_dec beta zero). + subst; now left. + specialize (H beta 1 (lt_succ beta)). assert (fin 1 o< succ beta). { destruct beta; destruct n0, n1. * now destruct n. * right; cbn; abstract lia. * destruct n0; cbn. left; auto. left; simpl;abstract lia. * left; simpl; abstract lia. } * specialize (H H0). rewrite <- succ_is_plus_1 in H. destruct (ON_mult.lt_strorder Omega Omega) as [H3 H4]. destruct (H3 _ H). Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)