proposition: Lemma oplus_strict_mono_0 : forall alpha, nf alpha -> forall a (Ha:nf a) b (Hb: nf b) c (Hc : nf c), lt a alpha -> lt c alpha -> lt b c -> lt (a o+ b) (a o+ c).
proof: Proof. Proof with eauto with T1. intros alpha ; transfinite_induction_lt alpha. clear alpha ; intros alpha Hrec Halpha; intros. destruct a. { now repeat rewrite oplus_0_l. } destruct b, c. - inversion H1. - rewrite oplus_0_r. now apply oplus_lt1. - T1_inversion H1. - nf_decomp Ha; nf_decomp Hb; nf_decomp Hc. rewrite ( oplus_eqn (cons a1 n a2) (cons b1 n0 b2)). rewrite ( oplus_eqn (cons a1 n a2) (cons c1 n1 c2)). case_eq (compare a1 b1). intro Ha1_b1; case_eq (compare a1 c1). { intro Ha1_c1. destruct (lt_inv H1). { apply compare_eq_iff in Ha1_b1 as <-, Ha1_c1 as <-. now apply lt_irrefl in H2. } destruct H2. destruct H2;subst c1. apply coeff_lt. auto with arith. decompose [and] H2; subst c1 n1. apply tail_lt. apply compare_eq_iff in Ha1_b1 as <-. apply Hrec with (phi0 a1); trivial. auto with T1. apply le_lt_trans with (cons a1 n a2) ; trivial. apply le_phi0. auto with T1. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; auto with T1. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro ; auto with T1. } { intro Ha1b1; rewrite compare_lt_iff in Ha1b1. apply compare_eq_iff in Ha1_b1 as <-. now apply head_lt. } { apply compare_eq_iff in Ha1_b1 as <-. intro H2. absurd (T1.lt (cons a1 n0 b2) (cons c1 n1 c2)). - apply lt_not_gt. apply head_lt. unfold T1.lt;rewrite compare_rev. now rewrite H2. - auto. } { intro. rewrite compare_lt_iff in H2. case_eq (compare a1 c1). { intro. apply compare_eq_iff in H3 as <-. absurd (T1.lt (cons b1 n0 b2) (cons a1 n1 c2));auto. apply lt_not_gt. apply head_lt; auto. } { intro. rewrite compare_lt_iff in H3. destruct (lt_eq_lt_dec b1 c1). destruct s. { apply head_lt; auto. } { subst c1. destruct (lt_inv_coeff_dec H1). { apply coeff_lt; auto. } destruct a; subst n1. apply tail_lt; auto. rewrite (oplus_eqn (cons a1 n a2) b2). rewrite (oplus_eqn (cons a1 n a2) c2). destruct b2,c2. T1_inversion H5. case_eq (compare a1 c2_1). intro. apply coeff_lt; auto with arith. intro H6; apply head_lt; unfold T1.lt; now rewrite H6. intros; apply tail_lt. apply oplus_lt1; trivial. T1_inversion H5. case_eq (compare a1 b2_1); case_eq (compare a1 c2_1); intros. { apply compare_eq_iff in H4 as <-, H6 as <-. destruct (lt_inv_coeff_dec H5). apply coeff_lt; auto with arith. destruct a;subst; apply tail_lt. apply Hrec with (phi0 a1); trivial. apply le_lt_trans with (cons a1 n a2);eauto with T1. apply le_phi0. eapply nf_inv2, nf2. eapply nf_inv2, nf4. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; eauto with T1. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; eauto with T1. } { apply compare_eq_iff in H6 as <-. now apply head_lt. } { apply compare_eq_iff in H6 as <-. apply compare_gt_iff in H4. exfalso. apply (@lt_trans c2_1 a1 b1) in H4 as Hgt; auto. now apply lt_inv_head, le_not_gt in H5. } { apply compare_eq_iff in H4 as <-. rewrite compare_lt_iff in H6. contradict H5; apply lt_not_gt; now apply head_lt. } { destruct (lt_inv H5). now apply head_lt. destruct H7. destruct H7;subst c2_1. now apply coeff_lt. decompose [and] H7. clear H7; subst. apply tail_lt. apply Hrec with (phi0 b1) ; trivial. apply le_lt_trans with (cons b1 n0 (cons c2_1 n2 c2_2)); trivial. apply le_phi0. eapply nf_inv2, nf2. eapply nf_inv2, nf4. auto with T1. apply lt_trans with (cons c2_1 n2 c2_2) ; trivial. apply tail_lt_cons; eauto with T1. eauto with T1. } { rewrite compare_lt_iff in H6. rewrite compare_gt_iff in H4. generalize(lt_inv_tail H1). intro. contradict H7; apply lt_not_gt; apply head_lt. eapply lt_trans;eauto. } { apply coeff_lt;auto with arith. } { now apply head_lt. } { apply tail_lt. apply Hrec with (phi0 a1) ; trivial. apply le_lt_trans with (cons a1 n a2). apply le_phi0; info_eauto with T1. auto with T1. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro, Ha. apply head_lt; now rewrite compare_gt_iff in H4. } } { contradict H1; apply lt_not_gt; now apply head_lt. } } { intro H3; rewrite compare_gt_iff in H3. contradict H1. apply lt_not_gt. apply head_lt; apply lt_trans with a1;auto. } } { intro. rewrite compare_gt_iff in H2. case_eq (compare a1 c1). intro. apply compare_eq_iff in H3 as <-. apply coeff_lt; auto with arith. intro H3; rewrite compare_lt_iff in H3. apply head_lt, H3. intro H3; rewrite compare_gt_iff in H3. apply tail_lt. apply Hrec with (phi0 a1) ; trivial. apply le_lt_trans with (cons a1 n a2) ; trivial. apply le_phi0 ; info_eauto with T1. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro;eauto with T1. auto with T1. } Unshelve. exact 0. exact 0. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)