proposition: Lemma gcdpE p q : gcdp p q = if size p < size q then gcdp (modp q p) p else gcdp (modp p q) q.
proof: Proof. pose gcdpE_rec := fix gcdpE_rec (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 gcdpE_rec n1 qq rr else rr. have Irec: forall k l p q, size q <= k -> size q <= l -> size q < size p -> gcdpE_rec k p q = gcdpE_rec l p q. + elim=> [|m Hrec] [|n] //= p1 q1. - move/size_poly_leq0P=> -> _; rewrite size_poly0 size_poly_gt0 modp0. by move/negPf ->; case: n => [|n] /=; rewrite mod0p eqxx. - move=> _ /size_poly_leq0P ->; rewrite size_poly0 size_poly_gt0 modp0. by move/negPf ->; case: m {Hrec} => [|m] /=; rewrite mod0p eqxx. case: eqP => Epq Sm Sn Sq //; have [->|nzq] := eqVneq q1 0. by case: n m {Sm Sn Hrec} => [|m] [|n] //=; rewrite mod0p eqxx. apply: Hrec; last by rewrite ltn_modp. by rewrite -ltnS (leq_trans _ Sm) // ltn_modp. by rewrite -ltnS (leq_trans _ Sn) // ltn_modp. have [->|nzp] := eqVneq p 0; first by rewrite mod0p modp0 gcd0p gcdp0 if_same. have [->|nzq] := eqVneq q 0; first by rewrite mod0p modp0 gcd0p gcdp0 if_same. rewrite /gcdp !ltn_modp !(negPf nzp, negPf nzq) /=. have [ltpq|leqp] := ltnP; rewrite !(negPf nzp, negPf nzq) /= polySpred //. have [->|nzqp] := eqVneq. by case: (size p) => [|[|s]]; rewrite /= modp0 (negPf nzp) // mod0p eqxx. apply: Irec => //; last by rewrite ltn_modp. by rewrite -ltnS -polySpred // (leq_trans _ ltpq) ?leqW // ltn_modp. by rewrite ltnW // ltn_modp. case: eqVneq => [->|nzpq]. by case: (size q) => [|[|s]]; rewrite /= modp0 (negPf nzq) // mod0p eqxx. apply: Irec => //; rewrite ?ltn_modp //. by rewrite -ltnS -polySpred // (leq_trans _ leqp) // ltn_modp. by rewrite ltnW // ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)