proposition: Lemma L alpha : 3 o<= alpha -> P alpha.
proof: Proof. pattern alpha; eapply well_founded_induction with E0lt. - apply E0lt_wf. - clear alpha; intro alpha. intros IHalpha Halpha. destruct (Zero_Limit_Succ_dec alpha) as [[H1 | H1] | H1]. + subst; rewrite Le_iff in Halpha. decompose [and] Halpha. cbn in Halpha. destruct Halpha as [H1 [H2 H3]]. rewrite le_lt_eq in H2; destruct H2; try discriminate. + red; intros; eapply L4; auto. + destruct H1; subst alpha. assert (H: 3 o<= x \/ x = E0fin 2). { destruct (le_lt_eq_dec Halpha). - left; destruct (E0_Lt_Succ_inv e). + apply Lt_Le_incl; auto. + subst; apply Le_refl. - right; revert e; ochange (E0fin 3) (E0_succ 2). intro; symmetry ; now apply Succ_inj. } destruct H. * apply L3; apply IHalpha; auto. -- apply Lt_Succ; auto. * subst x; ochange (E0_succ 2) (E0fin 3); apply P_3. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)