proposition: Lemma ruv i : r i = u i * r 0 + v i * r 1.
proof: Proof. elim/pair_ind: i => [||k [Hk1 Hk]]. by rewrite mul1r /= /v0 mul0r addr0. by rewrite /= /v1 mul1r mul0r add0r. rewrite /v uvE. transitivity (- q k.+2 * (u k.+1 * r 0 + v k.+1 * r 1) + (u k * r 0 + v k * r 1)). by rewrite -Hk -Hk1 (rE k) addrA addrC [in X in _ + X]addrC mulNr subrr addr0. rewrite mulrDl mulrDr mulrA -2!addrA; congr (_ + _). rewrite mulrDl [in RHS]addrC mulrA -addrA; congr (_ + _); by rewrite addrC. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)