proposition: Lemma ltn_size_r_stop l (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : 1 <= l < stop -> size (r l.+1) < size (r l).
proof: Proof. move=> lEu. apply Euclid.ltn_size_r => //. by case/andP : lEu. case/andP : lEu => l0. rewrite /stop. case: Bool.bool_dec => H1; last by rewrite tr0 in H1. case: Bool.bool_dec => H2; last by rewrite r1_leq_r0 in H2. rewrite /stop'; case: ex_maxnP => i Hi H li. move/forallP in Hi; move: (Hi (Ordinal li)). rewrite /= ltnNge; apply: contra => /eqP ->. by rewrite size_poly0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)