proposition: Lemma map_seqmul : forall (s c : seq R), all_pos c -> (size s = size c) -> map (fun x => x != 0) (seqmul s c) = map (fun x => x != 0) s.
proof: Proof. elim=> [c Hc Hsize |a s IHs]. by rewrite seqmul0. case=> [ | b l Hblpos Hsize] //. have/andP [Hb Hlpos] := Hblpos. rewrite seqmul_cons !map_cons mulIr_eq0. rewrite IHs //. by apply: eq_add_S. apply/rregP. rewrite lt0r in Hb. by case/andP : Hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)