proposition: Lemma root_sub_annihilant_creal (x y : creal) (p q : {poly F}) : (p != 0)%B -> (q != 0)%B -> p.[x] == 0 -> q.[y] == 0 -> (sub_annihilant p q).[x - y] == 0.
proof: Proof. move=> p_neq0 q_neq0 px_eq0 qy_eq0. have [||[u v] /= [hu hv] hpq] := @sub_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)) addrCA subrr addr0 split_norm_add // normrM. apply: le_lt_trans (_ : (ubound u.[y, x - y]) * `|p.[x i]| < _). by rewrite ler_wpmul2r ?normr_ge0 // (uboundP u.[y, x - y] 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]) * `|q.[y i]| < _). by rewrite ler_wpmul2r ?normr_ge0 // (uboundP v.[y, x - y] 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)