proposition: Lemma num_field_proj : {CtoQn | CtoQn 0 = 0 & cancel QnC CtoQn}.
proof: Proof. pose b := vbasis {:Qn}. have Qn_bC (u : {x | x \in Crat_span (map QnC b)}): {y | QnC y = sval u}. case: u => _ /= /Crat_spanP/sig_eqW[a ->]. exists (\sum_i a i *: b`_i); rewrite rmorph_sum /=; apply: eq_bigr => i _. by rewrite rmorphZ_num (nth_map 0) // -(size_map QnC). pose CtoQn x := oapp (fun u => sval (Qn_bC u)) 0 (insub x). suffices QnCK: cancel QnC CtoQn by exists CtoQn; rewrite // -(rmorph0 QnC) /=. move=> x; rewrite /CtoQn insubT => /= [|Qn_x]; last first. by case: (Qn_bC _) => x1 /= /fmorph_inj. rewrite (coord_vbasis (memvf x)) rmorph_sum rpred_sum //= => i _. rewrite rmorphZ_num Crat_spanZ ?mem_Crat_span // -/b. by rewrite -tnth_nth -tnth_map mem_tnth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)