proposition: Lemma adjoin0_deg : adjoin_degree K 0 = 1.
proof: Proof. by rewrite /adjoin_degree addv0 subfield_closed divnn adim_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)