proposition: Lemma alt_one_root2 (R : archiFieldType) (l : {poly R}) : alternate l -> one_root2 l 0.
proof: Proof. move/desc => [[x1 k] /= [/andP[x1p kp] neg] sl]; exists x1, k; split => //. - by move=> x xgt0 xlex1; apply: neg; rewrite xgt0 xlex1. - by move=> x y xlex1 xlty; apply: sl; rewrite xlex1 (ltW xlty). Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc