proposition: Lemma ltn_size_r_stop_r0 l (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : 1 <= l < stop -> size (r l.+1) < size (r 0).
proof: Proof. elim: l => // -[_ /=|l IH H]. 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 ij i1. move: Hi => /forallP /(_ (Ordinal i1)) H. by rewrite (leq_trans _ r1_leq_r0) // ltn_modpN0 // -size_poly_eq0 -lt0n (leq_trans _ H). rewrite (leq_trans (ltn_size_r_stop _ _ H)) // ltnW //. apply IH => /=. simpl in H. by rewrite ltnW. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)