1.8.0

• allow Coq 8.17, drop 8.14
• allow Mathcomp 1.16, drop 1.13-14
• add mathcomp-algebra dependency
• add Prop-level theory for All and Has
• rename AllPn->allPnIn, HasPn->hasPnIn
• add trans_eq, if_triv, theory for foldl/r and onth in prelude, rename prefixP -> prefixE
• expand seq theory in seqext, including "big cat" lemmas
• refactor slice theory, split interval theory on unique sequences into useqord, uslice and uconsec