proposition: Lemma bottom_element_no_lt : forall a b x y : E, is_bottom_element a b x -> lt a y x -> inc y b -> False.
proof: Proof. intros. unfold is_bottom_element in H; ee. unfold is_lower_bound in H; ee. assert (leq a x y). apply H5; am. apply no_lt_leq with a y x; au. Qed.
imports: universe