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