proposition: Lemma leq_size_v (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) k : (size r0).-1 <= t.*2 -> k.-1 < stop -> (size (v k)).-1 <= t.
proof: Proof. move=> r0t. case: k => [_|k]. by rewrite /= /Euclid.v0 size_poly0. move=> lEu. rewrite /= in lEu. rewrite size_v_sum //. rewrite -(leq_add2l t) addnn. move: (size_r0_sum tr0 r1_ltn_r0 lEu). rewrite [in X in X = _ -> _]/= => H. apply: (leq_trans _ r0t). rewrite [in X in _ <= X]H. rewrite addnC leq_add2l. move: lEu. 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 /stop'; case: ex_maxnP => i Pi Hi l'i. have : euclid_cont k. move: (euclid_back k i). by rewrite -ltnS Pi l'i. move/forallP/(_ (Ordinal (ltnSn k))) => H'. by rewrite -(leq_add2r 1) 2!addn1 prednK // (leq_ltn_trans _ H'). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)