proposition: Remark R28 : l = 0 -> (beta t1<= delta)%t1.
proof: Proof. intro H; apply R24; replace (n+l)%nat with n. - rewrite R14; auto. - rewrite H; auto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)