proposition: Lemma div_rec_polyE (p q : {poly R}) n r m: div_rec_poly (N:=nat) (R:=R) q n r p m = redivp_rec q n r p m.
proof: Proof. rewrite /div_rec_poly /redivp_rec. move: n r p. elim: m=> [|m ihm] n r p; by rewrite -[(_ < _)%C]/(_ < _) /shift_op /shift_poly /shiftp ?ihm mul_polyC [(_ + _)%C]addn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements hrel poly_op)