proposition: Lemma plus_assoc2 (gamma : Ord) : alpha + beta <= gamma -> exists khi, gamma = alpha + (beta + khi).
proof: Proof. intros H0; assert (H1 : alpha <= gamma). { apply le_trans with (alpha + beta);auto. apply le_plus_l; auto. } case (minus_exists H1); intros z Hz . assert (H2 :beta <= z). { tricho beta z HH. - right;auto. - left;auto. - case (@lt_irrefl gamma). pattern gamma at 1; rewrite <- Hz. apply lt_le_trans with (alpha + beta);auto. + apply plus_mono_r;auto. } case (minus_exists H2);intros u Hu. exists u;auto. rewrite Hu;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)