proposition: Lemma coprimep_linear_factor_seq p : forall (i j : 'I_(size (linear_factor_seq p))), i != j -> coprimep (linear_factor_seq p)`_i (linear_factor_seq p)`_j.
proof: Proof. move=> [i +] [j +]; rewrite !size_map=> Hi Hj Hij. rewrite !(nth_map (0,0%N)) ?size_map //. apply/coprimep_expl/coprimep_expr/coprimep_factor. by rewrite unitfE subr_eq0 !(nth_map 0) //= nth_uniq // ?undup_uniq // eq_sym. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)