proposition: Lemma root_div_annihilant_creal (x y : creal) (p q : {poly F}) (y_neq0 : y != 0) : (p != 0)%B -> (q != 0)%B -> p.[x] == 0 -> q.[y] == 0 -> (div_annihilant p q).[(x / y_neq0)%CR] == 0.
proof: Proof. move=> p_neq0 q_neq0 px_eq0 qy_eq0. have [||[u v] /= [hu hv] hpq] := @div_annihilant_in_ideal _ p q. + by rewrite (@has_root_creal_size_gt1 x). + by rewrite (@has_root_creal_size_gt1 y). apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi /=; rewrite subr0. rewrite (hpq (y i)) mulrCA divff ?mulr1; last first. by rewrite -normr_gt0 (lt_le_trans _ (lbound0_of y_neq0)) ?lbound_gt0. rewrite split_norm_add // normrM. apply: le_lt_trans (_ : (ubound u.[y, x / y_neq0]) * `|p.[x i]| < _). by rewrite ler_wpmul2r ?normr_ge0 // (uboundP u.[y, x / y_neq0] i). rewrite -ltr_pdivl_mull ?ubound_gt0 //. by rewrite (@eq0_modP _ px_eq0) // !pmulr_rgt0 ?gtr0E ?ubound_gt0. apply: le_lt_trans (_ : (ubound v.[y, x / y_neq0]) * `|q.[y i]| < _). by rewrite ler_wpmul2r ?normr_ge0 // (uboundP v.[y, x / y_neq0] i). rewrite -ltr_pdivl_mull ?ubound_gt0 //. by rewrite (@eq0_modP _ qy_eq0) // !pmulr_rgt0 ?gtr0E ?ubound_gt0. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)