proposition: Lemma size_r0_sum (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) l : l < stop -> (size (r 0)).-1 = (\sum_(k < l.+1) (size (q k.+1)).-1 + (size (r l)).-1)%nat.
proof: Proof. elim: l => [_ | l IH]. by rewrite big_ord_recr big_ord0 /= size_poly0. move=> lEu. rewrite IH; last by rewrite (ltn_trans (ltnSn _) lEu). transitivity ((\sum_(k < l.+1) (size (q k.+1)).-1 + (size (q l.+2)).-1 + (size (r l.+1)).-1)%N); last first. by rewrite [in RHS]big_ord_recr -addnA. rewrite -addnA. congr addn. have H1 : 0 < size (q l.+2) by rewrite (ltn_trans _ (ltn_size_q tr0 r1_ltn_r0 lEu)). have {}lEu : is_true (0 < l.+1 < stop) by rewrite lEu. rewrite Euclid.rE size_addl; last first. rewrite size_mul; last 2 first. by rewrite -size_poly_eq0 -lt0n. by rewrite -size_poly_eq0 -lt0n (leq_ltn_trans _ (ltn_size_r_stop tr0 (ltnW r1_ltn_r0) lEu)). suff : (forall a b c, 0 < b -> a < c -> (a < (b + c).-1))%nat. apply => //; by apply: (ltn_size_r_stop tr0 (ltnW r1_ltn_r0) lEu). clear. move=> a. case=> // b; case=> // c _ ac. by rewrite addSn /= ltn_addl. rewrite size_mul; last 2 first. by rewrite -size_poly_eq0 -lt0n. by rewrite -size_poly_eq0 -lt0n (leq_ltn_trans _ (ltn_size_r_stop tr0 (ltnW r1_ltn_r0) lEu)). suff : (forall a b, 0 < a -> 0 < b -> (a + b).-2 = a.-1 + b.-1)%nat. apply => //; by rewrite (leq_ltn_trans _ (ltn_size_r_stop tr0 (ltnW r1_ltn_r0) lEu)). clear. case=> // a; case => // b _ _. by rewrite addSn addnS. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)