proposition: Remark R19 : beta t1<= gamma.
proof: Proof. generalize Rem10; unfold P; fold gamma. intro H. destruct (compare gamma beta) eqn: Hcomp. - apply compare_eq_iff in Hcomp as ->. apply LE_refl. eapply LT_nf_r; eauto. - contradiction. - apply LE_r. rewrite compare_gt_iff in Hcomp; repeat split; auto. + eapply LT_nf_r; eauto. + subst gamma; eapply standard_gnaw_nf; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)