proposition: Lemma canon_limit_mono alpha i j : nf alpha -> T1limit alpha -> i < j -> canon alpha i t1< canon alpha j.
proof: Proof. pattern alpha ; apply transfinite_recursor_lt. clear alpha; intros alpha Hrec alpha_nf Hlim Hij. destruct alpha. - discriminate. - destruct (@T1.T1limit_cases _ _ _ alpha_nf Hlim) as [[H1 H2] | H3]. + subst; destruct n. * case_eq (T1limit alpha1). -- intro H; repeat rewrite canon_lim1; auto. ++ apply phi0_mono_strict_LT, Hrec; auto. apply lt_a_phi0_a. -- intro H; destruct (@zero_limit_succ_dec alpha1) ; trivial. ++ destruct s. ** contradiction. ** rewrite i0 in H; discriminate. ++ destruct s as [beta [Hbeta Hbeta']]; subst. destruct i, j. ** lia. ** rewrite canon0_phi0_succ_eqn, canonS_phi0_succ_eqn; auto. apply LT1; auto. ** lia. ** repeat rewrite canonS_phi0_succ_eqn; auto. apply LT3; auto. lia. * destruct (@zero_limit_succ_dec alpha1) ; trivial. -- destruct s. ++ subst; exfalso; now apply H1. ++ repeat rewrite canon_lim2; auto. apply LT4. ** apply nf_cons_LT;auto. apply canon_LT; auto. apply nf_phi0; auto. apply nf_canon; auto. ** apply nf_cons_LT; auto. apply canon_LT; auto. apply nf_phi0, nf_canon; auto. ** apply phi0_mono_strict_LT. apply Hrec; auto. apply head_lt_cons. -- destruct s as [beta [H2 H3]]. ++ subst; destruct i, j. ** lia. ** rewrite canonS_cons_succ_eqn2, canon0_cons_succ_eqn2; auto. apply LT4; auto. apply nf_cons_LT, LT_succ; auto. apply LT_succ; auto. apply LT1. apply single_nf; auto. ** lia. ** repeat rewrite canonS_cons_succ_eqn2; auto. apply LT4; auto. apply nf_cons_LT; auto. apply LT_succ; auto. apply nf_cons_LT; auto. apply LT_succ; auto. apply LT3; auto. lia. + destruct H3 as [H H0]. repeat rewrite canon_lim3; auto. * apply LT4. -- apply nf_tail_lt with alpha2; auto. apply canon_LT; auto. ++ eapply nf_inv2; eassumption. ++ apply T1limit_not_zero; auto. eapply nf_inv2; eassumption. -- apply nf_tail_lt with alpha2; auto. apply canon_LT; auto. eapply nf_inv2; eassumption. apply T1limit_not_zero; auto. eapply nf_inv2; eassumption. -- apply Hrec; auto. eapply nf_inv2; eauto. apply tail_lt_cons; auto. eapply nf_inv2; eauto. * eapply nf_inv1; eauto. * eapply nf_inv2; eauto. * eapply nf_inv1; eauto. * eapply nf_inv2; eauto. Qed.
imports: hydras.Prelude(DecPreOrder)