proposition: Lemma SortedT_dec T (R : T -> T -> Prop) l : (forall a b, decidable (R a b)) -> Sorted R l -> SortedT R l.
proof: Proof. move=> Hdec H0. elim: l H0 =>[//| a l] H0; first by left. have [Ral|Ral] := @HdRel_dec T R a l Hdec. - move=> SRal; constructor. + by apply H0; inversion SRal. + exact: HdRelT_dec. - move => K; constructor. + by apply: H0; inversion K. + by exfalso; apply: Ral; 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)