proposition: Lemma g_1_of : ordering_function g_1 (image B g) B.
proof: Proof. split. - apply L3a. - destruct 1 as [x [H0 H1]]. rewrite <- H1. replace (g_1 (g x)) with x; auto. symmetry;unfold g_1;eapply inv_compose;eauto. auto with schutte. - intros b H; exists (g b); split;auto. + exists b; split;auto. + unfold g_1;eapply inv_compose;eauto. auto with schutte. - intros; tricho (g_1 a) (g_1 b) Hab; auto with schutte. + case g_1_bij; intros. generalize (H2 a H). case g_1_bij; intros. generalize (H2 b H0). replace a with (g (g_1 a)) in H1. replace b with (g (g_1 b)) in H1. rewrite Hab in H1. case (@lt_irrefl _ H1). unfold g_1; apply inv_composeR; auto with schutte. unfold g_1; apply inv_composeR; auto with schutte. + case (le_not_gt (a:=a)(b:= b)); auto with schutte. replace a with (g (g_1 a)); replace b with (g (g_1 b)) . apply g_mono;auto with schutte. case g_1_bij;auto with schutte. case g_1_bij;auto with schutte. all : unfold g_1; apply inv_composeR; auto with schutte. Qed.
imports: ZornsLemma(CountableTypes)