proposition: Lemma redivp_rec_loopTP (k : nat * polyF * polyF -> fF) : (forall c qq r e, qf_eval e (k (c,qq,r)) = qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r)))) -> forall q sq cq c qq r n e (d := redivp_rec_loop (eval_poly e q) sq (eval e cq) c (eval_poly e qq) (eval_poly e r) n), qf_eval e (redivp_rec_loopT q sq cq c qq r n k) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
proof: Proof. move=> Pk q sq cq c qq r n e /=. elim: n c qq r k Pk e => [|n Pn] c qq r k Pk e; rewrite sizeTP. case ltrq : (_ < _); first by rewrite /= ltrq /= -Pk. rewrite lead_coefTP => [|a p]; rewrite Pk. rewrite ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=. by rewrite ltrq //= !mul_polyC ?(mul0r,add0r,scale0r). by symmetry; rewrite Pk ?(eval_mulpT,eval_amulXnT,eval_sumpT, eval_opppT). case ltrq : (_<_); first by rewrite /= ltrq Pk. rewrite lead_coefTP. rewrite Pn ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=. by rewrite ltrq //= !mul_polyC ?(mul0r,add0r,scale0r). rewrite -/redivp_rec_loopT => x e'. rewrite Pn; last by move=> *; rewrite Pk. symmetry; rewrite Pn; last by move=> *; rewrite Pk. rewrite Pk ?(eval_lift,eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT). by rewrite mul_polyC ?(mul0r,add0r). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)