proposition: Lemma solve_key_equation_coprimep p t : V * (r 1) = R + U * (r 0) -> size V <= p -> size R <= t -> (p + t = size r0)%N -> coprimep V R -> let stop := stop t (r 0) (r 1) in exists k, k <> 0 /\ v stop = k *: V /\ r stop = k *: R.
proof: Proof. move=> H1 Hmu Hnu H2 Hco j. have [l [l_neq0 [vvi rrj]]] := solve_key_equation H1 Hmu Hnu H2. move: Hco. rewrite {1}vvi {1}rrj coprimepMr coprimepMl coprimepp => /andP[/andP[]]. case/size_poly1P => k k_neq0 lk _ _. exists k^-1; split; first by apply/eqP; rewrite invr_eq0. split. - by rewrite vvi lk mul_polyC scalerA mulVr ?scale1r // unitfE. - by rewrite rrj lk mul_polyC scalerA mulVr ?scale1r // unitfE. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)