proposition: Lemma size_char_poly : size char_poly = n.+1.
proof: Proof. have [q <- lt_q_n] := split_diagA; have le_q_n := leq_trans lt_q_n (leq_pred n). by rewrite size_addl size_prod_XsubC size_diagA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)