proposition: Lemma size_v_incr_new i (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : 1 < i < stop -> size (v i) < size (v i.+1).
proof: Proof. case/andP => i1 istop. move: (relationF tr0 r1_leq_r0 istop) => H1. destruct i => //. move: (relationF tr0 r1_leq_r0(ltnW istop)) => H2. move: (ltn_size_r_stop). have H3 : 0 < i < stop. destruct i => //=. by rewrite ltnW. move/(_ _ tr0 r1_leq_r0 H3) => H4. move: H1. move/(congr1 (fun x => x.+1))/eqP. Abort. Lemma size_v_incr (tr0 : t < size r0) (r1_ltn_r0 : size r1 < size r0) i : i < stop -> size (v i) < size (v i.+1). Proof. elim: i => [_ /= | i ih istop]. by rewrite /Euclid.v0 /Euclid.v1 size_poly0 size_poly1. have Hq : 1 < size (q i.+2) by apply ltn_size_q. move=> [:H1 H2]. rewrite /Euclid.v Euclid.uvE mulNr size_addl size_opp. rewrite size_mul; last 2 first. abstract: H1; by rewrite -size_poly_eq0 -leqn0 -ltnNge (ltn_trans _ Hq). abstract: H2. rewrite -size_poly_eq0 -leqn0 -ltnNge (leq_ltn_trans _ (ih _)) //. by rewrite (ltn_trans _ istop). by rewrite -subn1 ltn_subRL ltn_add2r. rewrite size_mul // -subn1 ltn_subRL (@ltn_trans (1 + size (v i.+1))) //. by rewrite ltn_add2l ih // (ltn_trans _ istop). by rewrite ltn_add2r. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)