proposition: Lemma plus_of_succ (alpha beta : Ord) : alpha + (succ beta) = succ (alpha + beta).
proof: Proof. Proof with trivial. pattern (plus alpha); apply plus_elim ... intros plus_alpha Hp; assert (H1 :plus_alpha beta < plus_alpha (succ beta)). { eapply ordering_function_mono. apply Hp. split. split. apply lt_succ; auto. } generalize (@lt_succ_le (plus_alpha beta) (plus_alpha (succ beta))). intros H2. generalize (H2 H1); intro H5; case (le_disj H5) ; auto. intro H6;case Hp;intros H H3 H4 H7. case (H4 (succ (plus_alpha beta))). - red; apply le_trans with (plus_alpha beta). + generalize (H beta ); unfold In, ge. intro H9; apply H3. split. + right; apply lt_succ. - intros x [Hx Ex]. absurd ( beta < x /\ x < succ beta). + intro H8; decompose [and] H8;clear H8. assert (H8: succ beta <= x) by (apply lt_succ_le; eauto with schutte). case (@lt_irrefl (succ beta)). eapply le_lt_trans. apply H8. assumption. + split. * eapply ordering_function_monoR. apply Hp. split. assumption. rewrite Ex. auto with schutte. * rewrite <- Ex in H6; eapply ordering_function_monoR. apply Hp. assumption. split. assumption. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)