proposition: Lemma leq_size_r n : (forall k, k < n -> r k != 0) -> size (r n) <= size (r 0) - n.-1.
proof: Proof. elim/pair_ind: n => [_|_|n [H1 H2 H]]. by rewrite /= subn0. by rewrite /= subn0. rewrite [n.+1]lock /= -lock. move: (H _ (ltnSn n.+1)) => /(ltn_modpN0 (r n)) K. have rk_neq0 k : k < n.+1 -> r k != 0 by move=> kn; apply H; rewrite ltnW. move: (leq_trans K (H2 rk_neq0)); rewrite [in X in _ < X -> _]/= => ltn_size. rewrite subnS -ltnS prednK //; exact: leq_ltn_trans ltn_size. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)