proposition: Lemma karatsuba_recE n (p q : {poly R}) : karatsuba_rec (N:=nat) n p q = p * q.
proof: Proof. elim: n=> //= n ih in p q *; case: ifP=> // _; set m := minn _ _. rewrite [p in RHS](rdivp_eq (monicXn _ m)) [q in RHS](rdivp_eq (monicXn _ m)). rewrite /shift_op /shift_polyR /shiftp /implem /implem_nat /implem_id. simpC. rewrite !ih !(mulrDl, mulrDr, mulNr) mulnC exprM. rewrite -addrA -addrA -opprD [X in X + _ - _]addrC [in LHS]addrACA addrK. by rewrite !(commr_polyXn, mulrA, addrA). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)