proposition: Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq tF) : all (@rterm _) ps -> (GRing.holds (set_nth 0 e i x) (foldr (fun t : tF => GRing.And (t != 0)) GRing.True ps) <-> all (fun p => ~~root p x) (map (eval_poly e \o abstrX i) ps)).
proof: Proof. elim: ps => [|p ps ihps] //=. case/andP=> rp rps; rewrite rootE abstrXP //. constructor; first by case=> /eqP-> hps /=; apply/ihps. by case/andP=> pr psr; split; first apply/eqP=> //; 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)