proposition: Lemma relationA k : v k.+1 * r k - v k * r k.+1 = (- 1)^+k *: r0.
proof: Proof. elim: k => [|k IH]. by rewrite /= /v0 mul0r subr0 expr0 scale1r /v1 mul1r. rewrite {1}[k.+1]lock [in X in X * _ - _ = _]/= -lock. rewrite {5}[k.+1]lock [in X in _ - _ * X= _]/= -lock. move/eqP: (divp_eq (r k) (r k.+1)). rewrite addrC -subr_eq => /eqP <-. rewrite mulrDl mulrDr opprD addrA. rewrite mulrN mulNr opprK addrC !addrA mulNr mulrC mulrAC subrr add0r. by rewrite exprS -scalerA scaleN1r -IH opprB. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)