proposition: Lemma L04 : forall beta:T1, T1limit beta -> forall n, leq lt (\F (S n)) (Canon.canon beta (S n)).
proof: Proof. destruct beta. - discriminate. - cbn. destruct beta1. + discriminate. + destruct beta2. * destruct n0. -- cbn. destruct beta1_1; cbn. ++ destruct n1. ** reflexivity. ** intros; apply lt_incl_le. apply head_lt; auto with T1. ++ destruct (pred beta1_2). ** intros; apply lt_incl_le; apply head_lt; auto with T1. ** intros; apply lt_incl_le; apply head_lt. { destruct n1;cbn. destruct beta1_2; cbn. - destruct beta1_1_1; cbn. + destruct n0; cbn; auto with T1. + destruct (pred beta1_1_2); cbn; auto with T1. - destruct n0; cbn; auto with T1. - destruct beta1_2; auto with T1. + destruct beta1_1_1. * destruct n0; cbn; auto with T1. * destruct (pred beta1_1_2); cbn; auto with T1. } -- intros;apply lt_incl_le. destruct (pred (cons beta1_1 n1 beta1_2)). ++ apply head_lt; auto with T1. ++ apply head_lt; auto with T1. * intros; apply lt_incl_le. destruct n0. -- apply head_lt; auto with T1. -- apply head_lt; auto with T1. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)