proposition: Lemma elim_concl_eq : forall x y, (x < y \/ y < x -> False) -> x = y.
proof: Proof. intros x y H. destruct (Z_lt_le_dec x y). - exfalso. apply H ; auto. - destruct (Zle_lt_or_eq y x);auto. exfalso. apply H ; auto. Qed.
imports: ZArithRing ZArith_base