proposition: Lemma mkPX_ok l P i Q : (mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l).
proof: Proof. unfold mkPX. destruct P. - case ceqb_spec; intros H; simpl; try reflexivity. rewrite H, (morph0 CRmorph), mkPinj_ok; rsimpl. - reflexivity. - case Peq_spec; intros H; simpl; try reflexivity. rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory