proposition: Lemma Exercise1_15a9 x y: inc x (substrate r) -> inc y (substrate r) -> (lo_bounds r (singleton x) = lo_bounds r (singleton y)) -> x = y.
proof: Proof. move=> xsr ysr h. have /Zo_hi [_ p1] : (inc x (lo_bounds r (singleton y))). by rewrite -h; apply: Zo_i => //; split => // u /set1_P ->; order_tac. have /Zo_hi [_ p2] : (inc y (lo_bounds r (singleton x))). by rewrite h; apply: Zo_i => //; split => // v /set1_P ->; order_tac. move: (p2 _ (set1_1 x)) (p1 _ (set1_1 y)) => q1 q2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)