proposition: Lemma stop_is_after (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : size (r stop) <= t.
proof: Proof. 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. rewrite leqNgt; apply/negP => abs. suff /ij : euclid_cont i.+1 by rewrite ltnn. apply/forallP => /= x. case/boolP : (x == ord_max) => [/eqP->//|Hx]. have {}Hx : x < i.+1 by rewrite ltn_neqAle Hx /= -ltnS. by move/forallP : Hi => /(_ (Ordinal Hx)). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)