simplify; intros 7; cases H3;
cases H (_); cases (H8 y); apply H9; cases (H8 p);
lapply (H12 H1) as H13; apply (le_le_eq);
-[1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption;
-|2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;]
+[1: apply (le_transitive ??? H4); apply (Le≪ ? H13); assumption;
+|2: apply (le_transitive ???? H5); apply (Le≫ ? (eq_sym ??? H13)); assumption;]
qed.
interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space.