proposition: Lemma oplus_lt_0 : forall b, nf b -> T1.lt b (b o+ (cons a1 n a2)).
proof: Proof. Proof with eauto with T1. intros b ; transfinite_induction_lt b. intros x H1 H; destruct x. - simpl; auto with T1. - rewrite oplus_eqn;case_eq (compare x1 a1). + auto with T1 arith. + intros H2; apply head_lt. unfold T1.lt; now rewrite H2. + intro; apply tail_lt, H1 ; trivial. eapply nf_inv2, H. now apply tail_lt_cons. eapply nf_inv2, H. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)