fact: Definition redivp : {poly R} -> {poly R} -> nat * {poly R} * {poly R} := locked_with redivp_key redivp_expanded_def.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)