proposition: Lemma canon0_LT alpha : nf alpha -> alpha <> zero -> canon alpha 0 t1< alpha.
proof: Proof. transfinite_induction_lt alpha. clear alpha; intros alpha Hrec Halpha; destruct (zero_limit_succ_dec Halpha). - destruct s. + subst alpha; now destruct 1. + destruct alpha. * now destruct 1. * intros H; destruct (T1_eq_dec alpha1 zero). { subst. destruct n. - replace alpha2 with zero. + split;auto. simpl; constructor. split;simpl;constructor. + T1_inversion Halpha; auto. - replace alpha2 with zero. + simpl; split; constructor. apply finite_lt; auto with arith. apply nf_FS. + T1_inversion Halpha; auto. } destruct alpha2. { destruct n. { destruct (@zero_limit_succ_dec alpha1) ; trivial. - destruct s. + subst; now destruct n0. + rewrite canon_lim1. * split. -- apply single_nf; auto. destruct (Hrec alpha1) ; trivial. apply head_lt_cons ; auto. -- split; auto with T1. * auto with T1. * trivial. - destruct s. { destruct a. { subst; rewrite canon0_phi0_succ_eqn. - split. + auto with T1. + split; trivial. * auto with T1. - assumption. } } } destruct (@zero_limit_succ_dec alpha1) ; trivial. { destruct s. - subst; now destruct n0. - rewrite canon0_lim2. + split. { apply cons_nf ; trivial. - destruct (Hrec alpha1) ; eauto with T1. - apply single_nf. destruct (Hrec alpha1); trivial. apply head_lt_cons. } split. * apply coeff_lt; auto with arith. * auto with T1. + eapply nf_inv1, Halpha. + auto. } destruct s; subst. { destruct a; subst; rewrite canon0_cons_succ_eqn2. - split. { eauto with T1. } + split. { apply coeff_lt; auto with arith. } auto with T1. - auto. } } rewrite canon_tail. { split. { nf_decomp Halpha. apply nf_intro ; trivial. - destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. now apply head_lt. discriminate. - apply lt_a_phi0_b_phi0R. apply T1.lt_trans with (cons alpha2_1 n1 alpha2_2). + destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. apply head_lt; auto. * discriminate. * tauto. + apply lt_a_phi0_b_phi0. apply lt_a_phi0_b_intro with n;auto. } split. - nf_decomp Halpha. apply tail_lt. destruct (Hrec (cons alpha2_1 n1 alpha2_2)); auto. + auto with T1. + discriminate. + destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. eauto with T1. discriminate. tauto. - trivial. } eauto with T1. discriminate. - destruct s. { destruct a; subst. intros; rewrite canon_succ; auto. split; auto. split; auto; apply lt_succ; auto. } Qed.
imports: hydras.Prelude(DecPreOrder)