proposition: Lemma Cr_zero_inv : forall x, Cr zero x -> AP x.
proof: Proof. intros x H; destruct (Cr_inv zero x H) as [[_ H1] | [H2 H3]]. - tauto. - destruct (lt_irrefl H2). Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)