proposition: Lemma Finite_subset_has_lub : forall X:Ensemble nat, Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m.
proof: Proof. intros X H'; elim H'. - exists 0. apply Upper_Bound_definition. + unfold nat_po. simpl. apply triv_nat. + intros y H'0; elim H'0; auto with sets arith. - intros A H'0 H'1 x H'2; try assumption. elim H'1; intros x0 H'3; clear H'1. elim le_total_order. simpl. intro H'1; try assumption. lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith. generalize (H'4 x0 x). clear H'4. clear H'1. intro H'1; lapply H'1; [ intro H'4; elim H'4; [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ] | clear H'1 ]. + exists x. apply Upper_Bound_definition. * simpl. apply triv_nat. * intros y H'1; elim H'1. -- generalize le_trans. intro H'4; red in H'4. intros x1 H'6; try assumption. apply H'4 with (y := x0). ++ elim H'3; simpl; auto with sets arith. ++ trivial. -- intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial. + exists x0. apply Upper_Bound_definition. * unfold nat_po. simpl. apply triv_nat. * intros y H'1; elim H'1. -- intros x1 H'4; try assumption. elim H'3; simpl; auto with sets arith. -- intros x1 H'4; elim H'4; auto with sets arith. + red. intros x1 H'1; elim H'1; 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