proposition: Theorem seqp_refl : reflexive (poly A0 eqA ltM) seqP.
proof: Proof. Proof using plusA multA minusA invA divA cs A1. red in |- *. intros p; case p; simpl in |- *. intros x H'. apply eqp_refl. Qed.
imports: Coq(Arith Compare_dec)