proposition: Lemma CrealJ (C : numClosedFieldType) : {mono (@Num.conj_op C) : x / x \is Num.real}.
proof: Proof. suff realK : {homo (@Num.conj_op C) : x / x \is Num.real}. by move=> x; apply/idP/idP => /realK//; rewrite conjCK. by move=> x xreal; rewrite conj_Creal. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)