proposition: Lemma euclid_cont_size_r (r1_eq_r0 : size r1 <= size r0) : forall k, euclid_cont k -> k <= size (r 0).
proof: Proof. case/boolP : [exists k : 'I_(size r0).+1, (size (r k)) <= t] => [/existsP[k Hk i Hi]|]. have Pk : ~~ euclid_cont k. rewrite /= negb_forall; apply/existsP; exists ord_max => /=. by rewrite -ltnNge. have : forall j, euclid_cont j -> j < k. move=> j Pj. rewrite ltnNge; apply: contra Pk => kj. move: (euclid_back k j) => /implyP; rewrite Pj kj; by apply. move/(_ i Hi) => ik. rewrite /=. move: (ltn_ord k). rewrite ltnS. apply: (leq_trans). by rewrite -ltnS ltnW. rewrite negb_exists => /forallP abs i /forallP Pi. move: (Euclid.leq_size_r (r1_eq_r0)) => size_r. have {abs} : forall k : nat, k < (size r0).+1 -> r k != 0. move=> k Hk. rewrite -size_poly_eq0. rewrite /= in abs. move: (abs (Ordinal Hk)) => Ht. rewrite -ltnNge /= in Ht. rewrite -lt0n. by rewrite (leq_trans _ Ht). move/size_r => {size_r}. rewrite subnn leqn0 leqNgt => /eqP size_r0. apply/negP => abs. have {}abs : (size (r 0)).+1 < i.+1 by []. move: (Pi (Ordinal abs)). by rewrite /= size_r0 leqn0 -(negbK (_ == _)) -lt0n. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)