proposition: Lemma root_info_eqP : forall (R : eqType), Equality.axiom (root_info_eq R).
proof: Proof. by move => R [x|x y|x y|x y] [z |z t|z t|z t]; (apply: (iffP idP); first (rewrite //=; try (case/andP=> /eqP -> /eqP -> //); move=>/eqP ->)) => //; case=> -> //= -> /=; apply/andP; split. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype order) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(mxalgebra perm zmodp matrix ssrint) mathcomp(seq rat) pol square_free casteljau desc mathcomp(ssrnum ssrint realalg poly) poly_normal