proposition: Lemma Cr_lt : forall alpha beta, beta < alpha -> forall x, Cr alpha x -> Cr beta x.
proof: Proof. intros alpha beta H x H0. assert (H1 : zero < alpha). { apply le_lt_trans with beta; auto with schutte. } specialize (Cr_pos_inv H1); intro H2; specialize (H2 _ H0 _ H). apply A_Cr; tauto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)