proposition: Lemma ltn_size_v (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) i : i.+1 < stop -> size (v i) < size (- q i.+2 * v i.+1).
proof: Proof. move=> istop. have Hq : 1 < size (q i.+2) by apply ltn_size_q. rewrite mulNr size_opp. rewrite size_mul; last 2 first. by rewrite -size_poly_eq0 -leqn0 -ltnNge (ltn_trans _ Hq). rewrite -size_poly_eq0 -lt0n. by rewrite (leq_ltn_trans _ (@size_v_incr tr0 r1_ltn_r0 _ (ltn_trans (ltnSn _) istop))). rewrite -subn1 ltn_subRL (@ltn_trans (1 + size (v i.+1))) // ?ltn_add2r //. by rewrite ltn_add2l size_v_incr // (ltn_trans _ istop). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)