fact: Definition optimal (p:positive) (c : chain) := forall c', chain_correct p c' -> (chain_length c <= chain_length c')%nat.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)