proposition: Remark R29 : l <> 0.
proof: Proof. intro H; destruct (@LT_irrefl delta). - apply LT_LE_trans with beta;auto. + apply R25;auto. + apply R28;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)