proposition: Lemma ltn_size_q' i (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) : i < stop -> r i.+1 != 0 -> 1 < size (q i.+2).
proof: Proof. move=> istop Hr; rewrite Euclid.qE. case: i => [|i] in Hr istop *. by rewrite size_divp //= ltn_subRL addn1 prednK // lt0n size_poly_eq0. rewrite size_divp // ltn_subRL addn1 prednK; last by rewrite lt0n size_poly_eq0. by rewrite ltn_size_r_stop // ltnW. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)