proposition: Remark R25 : delta t1< beta.
proof: Proof. rewrite R22; generalize Rem11;unfold P; intro H. destruct(compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0. - contradict H; congruence. - rewrite compare_lt_iff in H0. repeat split;auto. + apply standard_gnaw_nf;auto. + eapply LT_nf_r; eauto. - contradict H; congruence. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)