proposition: Lemma plus_reg_r (alpha beta gamma : Ord) : alpha + beta = alpha + gamma -> beta = gamma.
proof: Proof. Proof with trivial. intros H; tricho beta gamma H0 ... - case (@lt_irrefl (alpha+beta)). pattern (alpha+beta) at 2; rewrite H; apply plus_mono_r ... - case (@lt_irrefl (alpha+beta)). pattern (alpha+beta) at 1; rewrite H; apply plus_mono_r ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)