proposition: Lemma CanonS_plus_1 alpha beta k i : beta <> E0zero -> alpha <> E0zero -> (beta o< E0_phi0 alpha)%e0 -> (Canon (Omega_term alpha i + beta)%e0 (S k) = (Omega_term alpha i + (Canon beta (S k)))%e0).
proof: Proof. intros; apply E0_eq_intro. rewrite Omega_term_plus; auto. - destruct alpha as [alpha Halpha]; destruct beta as [beta Hbeta]. red in H0;unfold E0.cnf; simpl in *. destruct beta. + destruct H; now apply E0_eq_intro. + destruct (compare alpha beta1) eqn:H2. * unfold lt in H1; simpl in H1. rewrite compare_eq_iff in H2; subst beta1. destruct (LT_inv H1). -- destruct (LT_irrefl H2). -- destruct H2. destruct H3. ++ inversion H3. ++ destruct H3 as [_ H4]; destruct (not_LT_zero H4). * red in H1; simpl in H1; destruct (LT_inv H1). -- destruct H3 as [_ [H4 _]]. now apply compare_lt_iff, lt_not_gt in H2. -- destruct H3. subst. destruct H4. ++ inversion H3. ++ destruct H3 as [_ H4]; destruct (not_LT_zero H4). * rewrite canon_tail; auto. -- apply cons_nf; auto with T1. rewrite compare_gt_iff in H2; auto. -- discriminate. - apply Lt_trans with beta; auto. apply CanonS_lt; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)