proposition: Lemma vu i : v i.+1 * u i - v i * u i.+1 = (- 1)^+i.
proof: Proof. elim: i => [|k IH]. by rewrite /= expr0 /v1 mul1r /u0 /v0 mul0r subr0. rewrite /v /u 2!uvE. transitivity ((- q k.+2 * v k.+1) * u k.+1 + v k * u k.+1 + v k.+1 * (q k.+2 * u k.+1) - v k.+1 * u k). rewrite mulrDl -3!addrA; congr (_ + (_ + _)). rewrite mulrDr opprD; congr (_ - _). by rewrite mulNr mulrN opprK. rewrite exprS -IH mulNr mul1r opprD opprK [in RHS]addrC; congr (_ - _). rewrite addrC addrA -[RHS]add0r; congr (_ + _). by rewrite mulrC -mulrA (mulrC (v k.+1)) mulrA 2!mulNr subrr. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)