proposition: Lemma g_bij : fun_bijection B (image B g) g.
proof: Proof. split. - intros a H ; exists a;split;auto. - red; destruct 1; exists x;split;auto. + case H;auto. + case H;auto. - red;intros a b; tricho a b Hab; trivial. intros H H0 ; generalize (g_mono H H0 Hab); auto. + intros H1 H2. rewrite H2 in H1; case (@lt_irrefl _ H1); auto. + intros H H0 H1; generalize (g_mono H0 H Hab); intro; rewrite H1 in H2; case (@lt_irrefl _ H2). Qed.
imports: ZornsLemma(CountableTypes)