proposition: Lemma holds_conj : forall e i x ps, all (@rterm _) ps -> (GRing.holds (set_nth 0 e i x) (foldr (fun t : tF => GRing.And (t == 0)) GRing.True%T ps) <-> all ((@root _)^~ x) (map (eval_poly e \o abstrX i) ps)).
proof: Proof. move=> e i x; elim=> [|p ps ihps] //=. case/andP=> rp rps; rewrite rootE abstrXP //. constructor; first by case=> -> hps; rewrite eqxx /=; apply/ihps. by case/andP; move/eqP=> -> psr; split=> //; apply/ihps. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)