proposition: Theorem eqp_trans : transitive _ eqP.
proof: Proof. Proof using plusA multA minusA invA divA cs A1 A0. red in |- *. intros x; elim x; auto. intros y z H'; inversion_clear H'. intros H'0; inversion_clear H'0; auto. intros a l H' y z H'0; inversion_clear H'0. intros H4; inversion_clear H4. change (eqP (pX a l) (pX mb0 q0)) in |- *; apply eqpP1; eauto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mb); auto. Qed.
imports: Coq(Arith Compare_dec)