proposition: Lemma g_mono : forall beta1 beta2, In B beta1 -> In B beta2 -> beta1 < beta2 -> g beta1 < g beta2.
proof: Proof. Proof with eauto with schutte. intros beta1 beta2 H H0 H1. assert( B2 : fun_bijection (members (g beta2)) (proper_segment_of B beta2) (_f beta2)) . { apply Ordering_bijection, g_lemma ... } assert (B3 : In (proper_segment_of B beta2) beta1). { split. apply H. split; assumption. } assert (B4 : exists alpha, alpha < g beta2 /\ _f beta2 alpha= beta1). { destruct B2; case (H3 beta1) ... } case B4; intros alpha (Ha2,Ha3). assert (B5 : ordering_function (_f beta2) (members alpha) (proper_segment_of B beta1)). { repeat split ... - red; intros; apply lt_trans with alpha0;eauto. - case B2;intros; clear H4 H5; red in H3. + generalize (H3 a); intros H4; clear H3; case H4. * red; apply lt_trans with alpha; auto. * auto. - case (g_lemma H0). intros H3 H4; decompose [and] H4; clear H4. replace beta1 with (_f beta2 alpha). intros. apply OF_mono0; auto. + red; apply lt_trans with alpha;auto. - destruct 1; case (g_lemma H0). intros H4 H5; decompose [and] H4; clear H4; decompose [and] H5. intros. case (OF_onto0 b). + split;auto. split;auto. eapply lt_trans;eauto. case H3;auto. + intros a (Ha,Ha');exists a;split;auto. red; tricho a alpha X. * auto. * subst a; rewrite Ha3 in Ha'. subst b; case H3;intros H33 _. case (@lt_irrefl _ H33). * assert (beta1 < b). { rewrite <- Ha3; rewrite <- Ha'. case (g_lemma H0); intros. apply OF_mono1; auto. } case (@lt_irrefl beta1); apply lt_trans with b;auto. case H3;auto. - intros; case (g_lemma H0); intros. apply OF_mono0; auto. red; apply lt_trans with alpha;auto. red; red; apply lt_trans with alpha;auto. } generalize (g_lemma H);intro. generalize (ordering_function_unicity B5 H2). destruct 1. generalize (Extensionality_Ensembles _ _ H3). intros; generalize (members_eq H5). intro; subst alpha;auto. Qed.
imports: ZornsLemma(CountableTypes)