intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml));
[apply (join ? pml)|apply (meet ? pml)
|3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);]
intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml));
[apply (join ? pml)|apply (meet ? pml)
|3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);]