proposition: Lemma ltn_size_q i (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) : i.+1 < stop -> 1 < size (q i.+2).
proof: Proof. move=> istop. apply: (ltn_size_q' tr0 r1_ltn_r0 (ltn_trans (ltnSn _) istop)). move: istop. rewrite /stop. case: Bool.bool_dec => H1; last by rewrite tr0 in H1. case: Bool.bool_dec => H2; last by rewrite (ltnW r1_ltn_r0) in H2. rewrite ltnS /stop'. case: ex_maxnP => l Hl Hi il. have : euclid_cont i.+1 by move: (euclid_back i.+1 l); rewrite Hl il. rewrite /euclid_cont /= => /forallP/(_ (Ordinal (ltnSn i.+1))). rewrite -size_poly_eq0; by case: (size _). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)