proposition: Lemma euclid_back i j : euclid_cont j && (i <= j) ==> euclid_cont i.
proof: Proof. apply/implyP => /andP [/forallP H1 H2]. apply/forallP => /= x. have @b : 'I_j.+1 by exists x; rewrite ltnS (leq_trans _ H2) // -ltnS. by rewrite (_ : r x = r b). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)