proposition: Theorem eqp_sym : symmetric _ eqP.
proof: Proof. Proof using plusA multA minusA invA divA cs A1 A0. red in |- *. intros x y H'; elim H'; auto. intros ma mb p q H H0 H1. apply eqpP1; auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.
imports: Coq(Arith Compare_dec)