proposition: Lemma rgcdpE p q : rgcdp p q = if size p < size q then rgcdp (rmodp q p) p else rgcdp (rmodp p q) q.
proof: Proof. pose rgcdp_rec := fix rgcdp_rec (n : nat) (pp qq : {poly R}) {struct n} := let rr := rmodp pp qq in if rr == 0 then qq else if n is n1.+1 then rgcdp_rec n1 qq rr else rr. have Irec: forall m n p q, size q <= m -> size q <= n -> size q < size p -> rgcdp_rec m p q = rgcdp_rec n p q. + elim=> [|m Hrec] [|n] //= p1 q1. - move/size_poly_leq0P=> -> _; rewrite size_poly0 size_poly_gt0 rmodp0. by move/negPf->; case: n => [|n] /=; rewrite rmod0p eqxx. - move=> _ /size_poly_leq0P ->; rewrite size_poly0 size_poly_gt0 rmodp0. by move/negPf->; case: m {Hrec} => [|m] /=; rewrite rmod0p eqxx. case: eqVneq => Epq Sm Sn Sq //; have [->|nzq] := eqVneq q1 0. by case: n m {Sm Sn Hrec} => [|m] [|n] //=; rewrite rmod0p eqxx. apply: Hrec; last by rewrite ltn_rmodp. by rewrite -ltnS (leq_trans _ Sm) // ltn_rmodp. by rewrite -ltnS (leq_trans _ Sn) // ltn_rmodp. have [->|nzp] := eqVneq p 0. by rewrite rmod0p rmodp0 rgcd0p rgcdp0 if_same. have [->|nzq] := eqVneq q 0. by rewrite rmod0p rmodp0 rgcd0p rgcdp0 if_same. rewrite /rgcdp -/rgcdp_rec !ltn_rmodp (negPf nzp) (negPf nzq) /=. have [ltpq|leqp] := ltnP; rewrite !(negPf nzp, negPf nzq) //= polySpred //=. have [->|nzqp] := eqVneq. by case: (size p) => [|[|s]]; rewrite /= rmodp0 (negPf nzp) // rmod0p eqxx. apply: Irec => //; last by rewrite ltn_rmodp. by rewrite -ltnS -polySpred // (leq_trans _ ltpq) ?leqW // ltn_rmodp. by rewrite ltnW // ltn_rmodp. have [->|nzpq] := eqVneq. by case: (size q) => [|[|s]]; rewrite /= rmodp0 (negPf nzq) // rmod0p eqxx. apply: Irec => //; last by rewrite ltn_rmodp. by rewrite -ltnS -polySpred // (leq_trans _ leqp) // ltn_rmodp. by rewrite ltnW // ltn_rmodp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)