proposition: Lemma size_rstop (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 Pi Hi. rewrite leqNgt. apply/negP => abs. have Pi1 : euclid_cont i.+1. rewrite /=. apply/forallP => x. move: (ltn_ord x). rewrite ltnS leq_eqVlt. case/orP => [/eqP ->{x} // | xi]. rewrite /euclid_cont /= in Pi. move/forallP in Pi. by move: (Pi (Ordinal xi)). move: (Hi _ Pi1). by rewrite ltnn. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)