proposition: Lemma reciprocal_eq (p q : {poly R}) : p`_0 != 0 -> q`_0 != 0 -> (p == q) = (reciprocal_pol p == reciprocal_pol q).
proof: Proof. move=> p0 q0; apply/idP/idP => [/eqP ->//|/eqP pq]. apply/eqP/poly_inj. have Hsize : size p = size q. by rewrite -reciprocal_size // -(@reciprocal_size q) // pq. apply: (@eq_from_nth _ 0) => // i ip. rewrite -reciprocal_nth_2// -(@reciprocal_nth_2 q) //. by rewrite pq Hsize. by rewrite -Hsize. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)