proposition: Lemma oplus_comm_0 (gamma: T1): nf gamma -> forall alpha beta, nf alpha -> nf beta -> T1.lt alpha gamma -> T1.lt beta gamma -> alpha o+ beta = beta o+ alpha.
proof: Proof. transfinite_induction gamma. intros x H0 H; destruct alpha, beta; try reflexivity. rewrite oplus_eqn. rewrite (oplus_eqn (cons beta1 n0 beta2) (cons alpha1 n alpha2)). repeat rewrite (compare_rev alpha1 beta1). intros Hnf_1 Hnf_2 Hlt_1 Hlt_2. nf_decomp Hnf_1; nf_decomp Hnf_2. destruct (compare alpha1 beta1) eqn:Hcomp; simpl CompOpp. - apply compare_eq_iff in Hcomp as <-. repeat rewrite (Nat.add_comm n n0); f_equal. + apply H0 with (phi0 alpha1); trivial. 2-3: apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n; eauto. apply LE_LT_trans with (cons alpha1 n0 beta2). * now apply LE_phi0. * now repeat split. - rewrite <- oplus_compare_Lt; auto. rewrite oplus_compare_Lt; auto. f_equal. apply H0 with (phi0 beta1) ; trivial. + apply LE_LT_trans with (cons beta1 n0 beta2). apply LE_phi0; auto. repeat split; trivial. + now apply head_lt, compare_lt_iff. + now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n. - rewrite <- oplus_compare_Gt; auto. rewrite oplus_compare_Gt; auto. f_equal; apply H0 with (phi0 alpha1); trivial. apply LE_LT_trans with (cons alpha1 n alpha2); trivial. + now apply LE_phi0. + repeat split; eauto with T1; apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n; eauto. + now apply head_lt, compare_gt_iff. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)