proposition: Lemma canonS_limit_strong lambda : nf lambda -> T1limit lambda -> forall beta, beta t1< lambda -> {i:nat | beta t1< canon lambda (S i)}.
proof: Proof. transfinite_induction lambda. clear lambda ; intros lambda Hrec Hlambda. intros H beta H1. assert (Hbeta: nf beta) by eauto with T1. destruct (zero_limit_succ_dec Hlambda). - destruct s. { subst lambda; inversion H1; destruct (not_LT_zero H1). } destruct lambda. + discriminate. + destruct (T1.T1limit_cases Hlambda i). { destruct a; subst lambda2; destruct beta. { exists 0; apply not_zero_lt. apply nf_canon; auto. apply T1limit_canonS_not_zero;auto. } destruct (LT_inv_strong H1). * destruct n. destruct (@zero_limit_succ_dec lambda1); trivial. -- destruct s. ++ subst; assert (False) by (eapply not_LT_zero; eauto). contradiction. ++ assert {i :nat | (beta1 t1< canon lambda1 (S i))%t1}. { apply Hrec. apply head_LT_cons; auto with T1. all: auto. } destruct H3 as [x l]. exists x; rewrite canonS_lim1; trivial; eauto with T1. -- destruct s as [x [H4 H5]]. subst lambda1; assert ({beta1 t1< x} + {beta1 = x})%t1. { apply LT_succ_LT_eq_dec in H2; trivial. eapply nf_inv1, Hbeta. } destruct H3. ++ exists 0; rewrite canonS_phi0_succ_eqn;auto with T1. ++ subst; exists (S n0); rewrite canonS_phi0_succ_eqn; auto. apply LT3; auto with arith. -- clear i; exists 0; rewrite canon_SSn_zero. ++ apply LT2; trivial. apply nf_intro; trivial. now apply nf_canon. apply lt_a_phi0_b_phi0R. apply canon_lt. eapply nf_coeff_irrelevance;eauto. discriminate. ++ eapply nf_inv1, Hlambda. * subst. -- destruct n. abstract lia. rewrite Nat.lt_succ_r in H3. destruct (Compare_dec.le_lt_eq_dec _ _ H3). exists 0; rewrite canon_SSn_zero. apply LT3; auto. { apply nf_intro; trivial. apply nf_canon; trivial. apply lt_a_phi0_b_phi0R. apply canon_lt. eapply nf_coeff_irrelevance;eauto. discriminate. } { eapply nf_inv1, Hlambda. } assert {i: nat | beta2 t1< (canon (cons lambda1 0 zero) (S i))}%t1. { apply Hrec. -- apply LT3;auto with arith. -- cbn; destruct lambda1. destruct H1; auto. auto. -- cbn; destruct lambda1. cbn in H; discriminate. auto. -- split. ++ eapply nf_inv2, Hbeta. ++ split. ** apply lt_a_phi0_b_phi0. apply lt_a_phi0_b_intro with n0;auto with T1. ** eapply nf_coeff_irrelevance;eauto. } subst; assert ({i: nat | beta2 t1< (canon (cons lambda1 0 zero) (S i))})%t1. { apply Hrec. - apply LT3;auto with arith. - cbn; destruct lambda1. + destruct H2;auto. + auto. - cbn; destruct lambda1. + destruct H2; auto. + auto. - split. + eapply nf_inv2, Hbeta. + split. * apply lt_a_phi0_b_phi0. apply lt_a_phi0_b_intro with n;auto with T1. * eapply nf_coeff_irrelevance;eauto. } destruct H4; exists x; rewrite canon_SSn_zero. apply LT4;auto. { apply nf_intro; auto with T1. eauto with T1. apply lt_a_phi0_b_phi0R. apply canon_lt. now apply nf_phi0. intro; subst; discriminate. } auto. * assert False by destruct (not_LT_zero H4); contradiction. } destruct a ; assert (lambda2 <> zero). { intro; subst; discriminate. } destruct beta. * exists 0; apply not_zero_lt. apply nf_canon; trivial; auto with T1. apply T1limit_canonS_not_zero; trivial. * destruct (LT_inv_strong H1). -- exists 0; rewrite canon_tail. apply LT2;auto. { apply nf_intro; trivial. eauto with T1. apply nf_canon; trivial; eauto with T1. apply lt_a_phi0_b_phi0R. apply T1.lt_trans with lambda2. apply canon_lt; eauto with T1. apply lt_a_phi0_b_phi0. apply lt_a_phi0_b_intro with n; eauto with T1. } auto. auto. -- destruct H4; exists 0; rewrite canon_tail. apply LT3; auto. { apply nf_intro. - eauto with T1. - apply nf_canon; eauto with T1. - apply lt_a_phi0_b_phi0R. apply T1.lt_trans with lambda2. apply canon_lt; eauto with T1. apply lt_a_phi0_b_phi0. apply lt_a_phi0_b_intro with n; eauto with T1. } all: auto. -- subst; assert ({i: nat | beta2 t1< (canon lambda2 (S i))})%t1. { apply Hrec. { apply tail_LT_cons; auto. } 1,2: eauto with T1. assumption. } destruct H4 as [x Hx]; exists x; rewrite canon_tail. apply LT4; auto. { apply nf_intro. eauto with T1. apply nf_canon; eauto with T1. apply lt_a_phi0_b_phi0R. apply T1.lt_trans with lambda2. apply canon_lt; eauto with T1. apply lt_a_phi0_b_phi0. apply lt_a_phi0_b_intro with n; eauto with T1. } all: auto. - destruct s as [t [Ht Ht']]; subst lambda. destruct (@T1limit_succ t); auto. Defined.
imports: hydras.Prelude(DecPreOrder)