proposition: Theorem seqp_sym : symmetric (poly A0 eqA ltM) seqP.
proof: Proof. Proof using plusA multA minusA invA divA cs A1. red in |- *. intros p q; case p; case q; simpl in |- *. intros x H' x0 H'0 H'1. apply eqp_sym; auto. Qed.
imports: Coq(Arith Compare_dec)