proposition: Theorem seqp_trans : transitive (poly A0 eqA ltM) seqP.
proof: Proof. Proof using plusA multA minusA invA divA cs A1. red in |- *. intros p q r; case p; case q; case r; simpl in |- *. intros x H' x0 H'0 x1 H'1 H'2 H'3. apply eqp_trans with (y := x0); auto. Qed.
imports: Coq(Arith Compare_dec)