proposition: Lemma ltn_size_r i : 1 <= i -> r i != 0 -> size (r i.+1) < size (r i).
proof: Proof. elim: i => // -[_ _ r10|k IH _ rn2]; first by rewrite /= ltn_modp. by rewrite {1}[k.+2]lock [in X in X < _]/= -lock ltn_modp. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)