proposition: Lemma HdRelT_dec T (R : T -> T -> Prop) a l : (forall a b, decidable (R a b)) -> HdRel R a l -> HdRelT R a l.
proof: Proof. move=> Hdec H0. elim: l H0 => [//|b l] H0; first by left. have [Rab|Rab] := Hdec a b. + by move=> ?; constructor. + by move=> K0; exfalso; inversion K0. 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)