proposition: Lemma lt_a_phi0_b_oplus : forall gamma alpha beta, alpha <_phi0 gamma -> beta <_phi0 gamma -> alpha o+ beta <_phi0 gamma.
proof: Proof. Proof with auto. induction gamma; destruct alpha, beta. - simpl; constructor. - inversion 2; inversion H5; now simpl. - inversion 1; T1_inversion H4. - inversion 1; T1_inversion H4. - simpl; auto. - simpl; auto. - simpl; auto. - rewrite oplus_eqn; case_eq (compare alpha1 beta1). + constructor; now inversion H0. + right; eapply lt_a_phi0_b_inv1;eauto. + right; eapply lt_a_phi0_b_inv1;eauto. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)