proposition: Lemma karatsuba_recE n (p q : {poly R}) : karatsuba_rec 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)). set dp := rdivp p _; set dq := rdivp q _; set rp := rmodp p _; set rq := rmodp q _. rewrite /shift_poly /split_poly !ih !(mulrDr, mulrDl, mulNr) mulnC exprM. rewrite -[_ - _ - _]addrA [_ + _ + (- _ - _)]addrACA [_ + _ - _]addrAC. by rewrite subrr add0r addrK !(commr_polyXn, mulrA, addrA). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(zmodp path choice fintype tuple finset ssralg) mathcomp(bigop poly polydiv)