proposition: Lemma po_st : forall X eq le mnt ant, @is_PartialOrder X eq le mnt ant -> Setoid_Theory X eq.
proof: Proof. Proof with trivial. intros X eq le0 mnt ant H. split. firstorder. intros x y E. apply (po_equiv_le_def H), and_comm, (po_equiv_le_def H)... intros x y z. repeat rewrite ->(po_equiv_le_def H). firstorder. Qed.
imports: CoRN.algebra.RSetoid