proposition: Lemma stop'_is_before (tr0 : t < size r0) (r1_leq_r0 : size r1 <= size r0) : t < size (r (stop' tr0 r1_leq_r0)).
proof: Proof. rewrite /stop'; case: ex_maxnP => i Hi _. move: Hi; by rewrite /euclid_cont => /forallP /(_ (Ordinal (ltnSn i))). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)