proposition: Lemma solve_key_equation m t : V * (r 1) = R + U * (r 0) -> size V <= m -> size R <= t -> (m + t = size r0)%N -> let j := stop t r0 r1 in exists k, k <> 0 /\ V = k * v j /\ R = k * r j.
proof: Proof. have r0_neq0 : r0 != 0. by rewrite -size_poly_eq0 -lt0n (leq_trans _ r1_leq_r0) // lt0n size_poly_eq0. move=> key_eqn Hmu Hnu Hsize j'. move: (euclid_lemma Hsize) => [H2 Hj]. set j := stop _ _ _ in H2, Hj. move: (Euclid.ruv r0 r1 j) => E1. have {}key_eqn : R = (- U) * r0 + V * r1 by rewrite key_eqn addrC mulNr addrK. move/(congr1 (fun x => V * x)) : (E1); rewrite mulrDr !mulrA => E1'. move/(congr1 (fun x => v j * x)) : (key_eqn); rewrite mulrDr !mulrA => key_eqn'. have step1 : r j * V = R * v j. have [k Hk] : exists k, r j * V = R * v j + k * r0. exists (V * u j - v j * (- U)). rewrite mulrC {}E1'. move: key_eqn' => /eqP. rewrite addrC -subr_eq -(mulrA _ V) mulrCA mulrA => /eqP <-. by rewrite addrCA mulrN mulNr 2!opprK -mulrDl mulrC. have HrV : size (r j * V) < size r0. case/boolP : (r j == 0) => [/eqP->|rj0]. by rewrite mul0r size_poly0 lt0n size_poly_eq0. case/boolP : (V == 0) => [/eqP ->|V_neq0]. by rewrite mulr0 size_poly0 lt0n size_poly_eq0. rewrite size_mul; last 2 first. exact: rj0. exact V_neq0. rewrite -Hsize. rewrite prednK; last first. by rewrite ltn_addr // lt0n size_poly_eq0. by rewrite addnC leq_add. have HRv : size (R * v j) < size r0. case/boolP : (v j == 0) => [/eqP->|vj0]. by rewrite mulr0 size_poly0 lt0n size_poly_eq0. case/boolP : (R == 0) => [/eqP->|R_neq0]. by rewrite mul0r size_poly0 lt0n size_poly_eq0. rewrite size_mul; last 2 first. exact R_neq0. exact vj0. rewrite prednK; last first. by rewrite addnC ltn_addr // lt0n size_poly_eq0. by rewrite -Hsize addnC leq_add. case/boolP : (k == 0) => [/eqP k0|k0]. move: Hk; by rewrite k0 mul0r addr0. exfalso. move/eqP : Hk. rewrite addrC -subr_eq. move/eqP/(congr1 (fun x : {poly F} => size x)). apply/eqP. rewrite ltn_eqF //. rewrite (leq_ltn_trans (size_add _ _)) // size_opp. rewrite (@leq_trans (size r0)) //. by rewrite gtn_max HrV. by rewrite size_mul // addnC -subn1 -addnBA ?lt0n ?size_poly_eq0 // leq_addr. have step2 : u j * V = (-U) * v j. move: step1. rewrite [in X in _ = X -> _]mulrC {}key_eqn' mulrC {}E1'. rewrite -(mulrA _ (v j)) mulrCA mulrA. move/eqP; rewrite -subr_eq addrK -subr_eq0 -mulrBl => /eqP. move/poly_idomainAxiom; rewrite (negbTE r0_neq0) orbF subr_eq0 => /eqP. rewrite mulrC => ->; by rewrite mulrC. have [l [Hl1 Hl2]] : exists l, (-U) = l * u j /\ V = l * v j. have Hcoprime : coprimep (u j) (v j). apply/Bezout_coprimepP. exists (v j.+1, - u j.+1). rewrite mulNr (mulrC _ (v j)) (Euclid.vu r0 r1 j). by rewrite /eqp dvd1p andbT dvdp1 -(mulr1 ((_)^+_)) size_Msign size_poly1. have /dvdpP[k Hk] : u j %| (-U). by rewrite -(Gauss_dvdpl _ Hcoprime) -step2 dvdp_mulr. have /dvdpP[k' Hk'] : v j %| V. rewrite -(@Gauss_dvdpl _ _ (u j)); last by rewrite coprimep_sym. by rewrite mulrC step2 dvdp_mull. case/boolP : (u j == 0) => [/eqP uj0|uj0]. move: Hcoprime. rewrite uj0 coprime0p => vj1. exists k'. by rewrite Hk uj0 2!mulr0. exists k; split => //. suff : k = k' by move => ->. move: step2. rewrite Hk Hk' mulrCA -mulrA => /eqP. rewrite -subr_eq0 -mulrBl => /eqP. move/poly_idomainAxiom => /orP[|/eqP]; first by rewrite subr_eq0 => /eqP. move/poly_idomainAxiom => /orP[] /eqP abs; last first. move: Hk'; rewrite abs mulr0 => /eqP; by rewrite (negbTE v_neq0). by rewrite abs eqxx in uj0. exists l; split. move=> ?; subst l. rewrite mul0r in Hl2. move: v_neq0. by rewrite Hl2 eqxx. move: key_eqn; by rewrite Hl1 Hl2 -!mulrA -mulrDr -E1. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)