proposition: Lemma r10_stop'0 (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : r1 = 0 -> stop' tr0 r1_leq_r0 = O.
proof: Proof. move=> r10; rewrite /stop'; case: ex_maxnP => i Pi Hi. have P1 : ~~ euclid_cont 1%nat. rewrite /= negb_forall. apply/existsP; exists (lift ord0 ord0). by rewrite /= r10 size_poly0 leqn0 -lt0n. case: i Pi Hi => // i Pi Hi. move: (euclid_next 1 i.+1). by rewrite P1 Pi. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)