fact: Definition gcdp p q := let: (p1, q1) := if size p < size q then (q, p) else (p, q) in if p1 == 0 then q1 else let fix loop (n : nat) (pp qq : {poly R}) {struct n} := let rr := modp pp qq in if rr == 0 then qq else if n is n1.+1 then loop n1 qq rr else rr in loop (size p1) p1 q1.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)