proposition: Lemma conjC_ge0 x : (0 <= x^* ) = (0 <= x).
proof: Proof. wlog suffices: x / 0 <= x -> 0 <= x^*. by move=> IH; apply/idP/idP=> /IH; rewrite ?conjCK. rewrite [in X in X -> _]le0r => /predU1P[-> | x_gt0]; first by rewrite rmorph0. by rewrite -(pmulr_rge0 _ x_gt0) mul_conjC_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)