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;]
+|2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;]
qed.
-interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space.
+interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space.