proposition: Lemma size_v_sum (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) k : k < stop -> (size (v k.+1)).-1 = (\sum_(i < k.+1) (size (q i.+1)).-1)%N.
proof: Proof. elim: k => [_ | k IH kstop]. by rewrite big_ord_recr /= big_ord0 /Euclid.v1 size_poly1 size_poly0. transitivity ((size (q k.+2)).-1 + (size (v k.+1)).-1)%N; last first. rewrite {}IH ?(ltn_trans _ kstop) //. by rewrite [in RHS]big_ord_recr addnC. rewrite {1}/Euclid.v Euclid.uvE size_addl; last by rewrite ltn_size_v. rewrite mulNr size_opp. have H1 : 0 < size (q k.+2) by rewrite (ltn_trans _ (ltn_size_q tr0 r1_ltn_r0 kstop)). have H2 : 0 < size (v k.+1). by rewrite (leq_ltn_trans _ (@size_v_incr tr0 r1_ltn_r0 _ (ltn_trans (ltnSn _) kstop))). rewrite size_mul -?size_poly_eq0 -?lt0n //. suff : (forall a b, 0 < a -> 0 < b -> (a + b).-2 = a.-1 + b.-1)%N by apply. case=> // a; case => // b _ _; by rewrite addSn addnS. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)