proposition: Lemma oplus_lt_rw2 : forall a n b x, nf (cons a n b) -> nf x -> x <_phi0 a -> cons a n b o+ x = cons a n (b o+ x).
proof: Proof. destruct x. - now (intros; repeat rewrite oplus_0_r). - intros; rewrite (oplus_eqn (cons a n b) (cons x1 n0 x2)). apply lt_a_phi0_b_phi0 in H1. destruct (lt_inv H1). + unfold T1.lt in H2. rewrite compare_rev, H2. reflexivity. + decompose [or and] H2. * inversion H5. * T1_inversion H6. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)