proposition: Remark R26 : ~ const_pathS (n+l) gamma beta.
proof: Proof. intro H; destruct (@LT_irrefl delta). apply LT_LE_trans with beta;auto. - apply R25;auto. - apply R24;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)