proposition: Lemma relationF k (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : k < stop -> ((size (v k.+1)).-1 + (size (r k)).-1 = (size (r 0)).-1)%N.
proof: Proof. elim: k => [?|k IH H]. by rewrite /= /Euclid.v1 /Euclid.v0 size_poly1 add0n. rewrite {1}/Euclid.v Euclid.uvE -2!/(Euclid.v _ _ _) Euclid.qE. have rk1_neq0 : r k.+1 != 0. move: H; 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 => i Hi ij ki. move: Hi => /forallP/(_ (Ordinal ki)) H. by rewrite -size_poly_eq0 -lt0n (leq_trans _ H). have rk_neq0 : r k != 0. move: H; 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 => i Hi ij ki. move: Hi => /forallP/(_ (Ordinal (ltnW ki))) H. by rewrite -size_poly_eq0 -lt0n (leq_trans _ H). have vk1_neq0 : v k.+1 != 0. destruct k; first by rewrite /= oner_neq0. rewrite -size_poly_eq0. apply/eqP => abs. move: {IH}(IH (ltnW H)); rewrite abs add0n => /(congr1 (fun x => x.+1)). rewrite prednK; last by rewrite lt0n size_poly_eq0. rewrite prednK; last by rewrite (leq_trans _ tr0). apply/eqP; rewrite ltn_eqF //. destruct k. move: abs. rewrite /= addr0 mulr1 size_opp => /eqP. rewrite size_poly_eq0 divp_eq0 ltnNge r1_leq_r0 orbF (negbTE rk_neq0) orbF. rewrite -size_poly_eq0 => abs. exfalso. move/eqP : abs; apply/eqP. by rewrite -lt0n (leq_trans _ tr0). by rewrite (ltn_size_r_stop_r0) //= ltnW // ltnW. rewrite size_addl; last first. rewrite mulNr size_opp. destruct k. rewrite /= /Euclid.v0 /Euclid.v1 size_poly0 mulr1 lt0n size_poly_eq0 divp_eq0. by rewrite ltnNge r1_leq_r0 orbF (negbTE rk1_neq0) orbF. have q_k3 : 1 < size (q k.+3). rewrite Euclid.qE size_divp // -subn1 subnBA; last by rewrite lt0n size_poly_eq0. rewrite addn1 subSn; last by rewrite ltnW // ltn_size_r_stop //= ltnW. by rewrite ltnS subn_gt0 ltn_size_r_stop //= ltnW. rewrite -Euclid.qE size_mul //; last first. by rewrite -size_poly_eq0 -lt0n (leq_trans _ q_k3). rewrite -subn1 -addnBA; last by rewrite lt0n size_poly_eq0. rewrite (@leq_ltn_trans (1 + (size (v k.+2)).-1))%N //. rewrite add1n prednK; last by rewrite lt0n size_poly_eq0. by rewrite leq_size_v_incr // ltnW. rewrite add1n subn1 prednK; last by rewrite lt0n size_poly_eq0. rewrite -subn1 addnBA ?lt0n ?size_poly_eq0 // (@leq_ltn_trans (1 + size (v k.+2) - 1)) //. by rewrite add1n subn1. by rewrite -addnBA ?lt0n ?size_poly_eq0 // -addnBA ?lt0n ?size_poly_eq0 // ltn_add2r. have H1 : size (r k.+1) <= size (r k). destruct k => //. by rewrite ltnW // ltn_size_r_stop //= ltnW. rewrite size_mul //; last by rewrite oppr_eq0 divpN0. rewrite size_opp size_divp // -subn2. set a := size (r k.+1). rewrite addnC addnBA; last first. rewrite {}/a -subn1 subnBA; last by rewrite lt0n size_poly_eq0. by rewrite addn1 subSn // addSn ltnS addn_gt0 (lt0n (size (v k.+1))) size_poly_eq0 vk1_neq0 orbT. rewrite addnA subnKC; last by rewrite {}/a (leq_trans _ H1) // leq_pred. rewrite -IH; last by rewrite ltnW. rewrite -[in X in (_ = _ + X)%N]subn1 addnBA; last by rewrite lt0n size_poly_eq0. rewrite [in RHS]addnC subn1 subn2; congr (_ .-1). rewrite -subn1 -addnBA; last by rewrite lt0n size_poly_eq0. by rewrite subn1. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)