proposition: Lemma Integers_has_no_ub : ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
proof: Proof. red; intro H'; elim H'. intros x H'0. elim H'0; intros H'1 H'2. cut (In nat Integers (S x)). - intro H'3. specialize H'2 with (y := S x); lapply H'2; [ intro H'5; clear H'2 | try assumption; clear H'2 ]. apply Nat.nle_succ_diag_l in H'5; assumption. - apply triv_nat. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image Infinite_sets Compare_dec Relations_1 Partial_Order Cpo