proposition: Lemma leq_size_v_incr i (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : i < stop -> size (v i) <= size (v i.+1).
proof: Proof. elim: i => [? /= | i ih istop]. by rewrite /Euclid.v0 /Euclid.v1 size_poly0 size_poly1. rewrite {2}/Euclid.v Euclid.uvE. do 2 rewrite -/(Euclid.v _ _ _). case/boolP : (v i.+1 == 0) => vi1_eq0. by rewrite (eqP vi1_eq0) size_poly0. destruct i. rewrite /= /Euclid.v0 /Euclid.v1 size_poly1 addr0 mulr1 size_opp. have r10 : r1 != 0. move: istop. 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 => l Hl Hi il. move: Hl => /forallP /(_ (Ordinal il)) H. by rewrite -size_poly_eq0 -lt0n (leq_trans _ H). rewrite size_divp //. rewrite -subn1 subnBA; last by rewrite lt0n size_poly_eq0. by rewrite addnC addSn add0n subSn. have ri20 : r i.+2 != 0. move: istop. 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 => l Hl Hi il. move: Hl => /forallP /(_ (Ordinal il)) H. by rewrite -size_poly_eq0 -lt0n (leq_trans _ H). have qi3 : 1 < size (q i.+3). rewrite {1}Euclid.qE size_divp //. rewrite -subn1 subnBA ?lt0n ?size_poly_eq0 // addn1 subSn; last first. by rewrite ltnW // ltn_size_r_stop //= ltnW. by rewrite ltnS subn_gt0 ltn_size_r_stop //= ltnW. rewrite [in X in _ <= X]size_addl. rewrite mulNr size_opp size_mul //; last first. by rewrite -size_poly_eq0 -lt0n (leq_trans _ qi3). rewrite -subn1 -addnBA; last by rewrite lt0n size_poly_eq0. rewrite (@leq_trans (1 + (size (v i.+2) - 1))) //. by rewrite add1n subn1 prednK // lt0n size_poly_eq0. by rewrite leq_add2r (leq_trans _ qi3). rewrite mulNr size_opp. rewrite size_mul // -?size_poly_eq0 -?lt0n ?(leq_trans _ qi3) //. rewrite -subn1 -addnBA; last by rewrite lt0n size_poly_eq0. rewrite (@leq_ltn_trans (1 + (size (v i.+2) - 1))) //; last first. by rewrite ltn_add2r. rewrite add1n subn1 prednK // ?lt0n ?size_poly_eq0 // ih //. by rewrite ltnW. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)