proposition: Lemma extend_cfConjC_subset S X phi : cfConjC_closed S -> ~~ has cfReal S -> phi \in S -> phi \notin X -> cfConjC_subset X S -> cfConjC_subset [:: phi, phi^* & X]%CF S.
proof: Proof. move=> ccS nrS Sphi X'phi [uniqX /allP-sXS ccX]. split; last 1 [by apply/allP; rewrite /= Sphi ccS | apply/allP]; rewrite /= inE. by rewrite negb_or X'phi eq_sym (hasPn nrS) // (contra (ccX _)) ?cfConjCK. by rewrite cfConjCK !mem_head orbT; apply/allP=> xi Xxi; rewrite !inE ccX ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)