proposition: Lemma char_poly_monic : monic n char_poly.
proof: Proof. rewrite /char_poly /determinant /matrixC. move: n A. clear n A. case=>[|n]=>A. have -> : index_enum (perm_for_finType (ordinal_finType 0)) = [::perm_one (ordinal_finType 0)]; last first. rewrite /= odd_perm1 /=. apply (monic_wd _ One); last by apply monic_c_one. rewrite /index_enum -enumT. have <- : [::] = enum (ordinal_finType 0); last first. by change ((One : CR[X])[=]One[*]One[+]Zero); ring. rewrite <- enum0. by apply eq_enum; case. rewrite /index_enum -enumT. have := (enum1 (perm_one (ordinal_finType 0)))=> /= <-. apply (@eq_enum _ 'S_0)=> s /=. symmetry. apply/eqP. apply/permP=> x. by case:x. apply (monic_bigsum (i:=perm_one (ordinal_finType n.+1)) (F:=fun s => _)). rewrite odd_perm1 /=. change (n.+1) with (0 + n.+1). apply monic_mult; first by apply monic_c_one. have : n.+1 = \big[addn/0]_(i<n.+1) 1. symmetry. setoid_rewrite big_const_ord. clear A; revert n. elim; first by done. by move=> n /= ->. move => Heq. rewrite -> Heq at 1. apply monic_bigprod=> i. rewrite /scalar_mx /addmx /oppmx perm1 eq_refl. split; first by rewrite -> nth_coeff_plus; reflexivity. apply degree_le_plus; first by apply degree_le_x_. change (degree_le 1 [--](_C_(A i i))). apply degree_le_inv. apply (degree_le_mon _ _ 0); first by apply le_S; apply le_n. by apply degree_le_c_. move=> s neq. change n with (0 + n). apply degree_le_mult. change (One : CR[X]) with (_C_ (One : CR)). case: (odd_perm s)=> /=; last by apply degree_le_c_. change (degree_le 0 ([--](_C_ One)[*](_C_ (One : CR)))). change 0 with (0 + 0). by apply degree_le_mult; [apply degree_le_inv|]; apply degree_le_c_. have: existsb i : ordinal_finType n.+1, s i != i. apply/forallP=> Heq. case: (negP neq)=> {neq}. apply/eqP. apply/permP=> x. rewrite perm1. apply/eqP. by apply Heq. case/existsP=> j Hj. setoid_rewrite (bigD1 (j:=j)); last by done. change n with (0 + n). apply degree_le_mult=> [|/=]. rewrite /scalar_mx /addmx /oppmx eq_sym (negbTE Hj). setoid_rewrite cm_lft_unit. apply degree_le_inv. by apply degree_le_c_. change (0 + n) with n. have Heq : n = \big[addn/0]_(i|i!=j) 1. setoid_rewrite big_const_seq; clear. have -> : count (predC (pred1 j)) (index_enum (ordinal_finType n.+1)) = n; last first. move=> {j}; revert n. by elim; [|move=> n /= <-]. have := (count_predC (pred1 j) (index_enum (ordinal_finType n.+1))). rewrite enumP /index_enum -enumT size_enum_ord /= add1n. by move/eqP; rewrite eqSS; move/eqP. rewrite {1}Heq=> {Heq}. apply bigprod_degree_le=> i Hneq. rewrite /scalar_mx /addmx /oppmx. apply degree_le_plus. case: (i == s i); first by apply degree_le_x_. apply (degree_le_mon _ _ 0); first by apply le_S; apply le_n. by move=> n' _; apply nth_coeff_zero. change (degree_le 1 ([--](_C_(A i (s i))))). apply degree_le_inv. apply (degree_le_mon _ _ 0); first by apply le_S; apply le_n. by apply degree_le_c_. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass