proposition: Lemma relationB k : u k.+1 * r k - u k * r k.+1 = (- 1)^+k.+1 *: r1.
proof: Proof. elim: k => [|k IH]. by rewrite /= /u1 /u0 mul0r add0r mul1r expr1 scaleN1r. 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)