proposition: Lemma Sorted_dec T (R : T -> T -> Prop) l : (forall a b, decidable (R a b)) -> decidable (Sorted R l).
proof: Proof. move=> Hdec. elim: l =>[//| a l [IHl|IHl]]; first by left. have [Ral|Ral] := @HdRel_dec T R a l Hdec. - left; constructor =>//. - by right => K; apply: Ral; inversion K. - by right => K; apply: IHl; inversion K. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)