proposition: Lemma Zlt_asymmetric : forall a b : Z, {(a < b)%Z} + {a = b} + {(a > b)%Z}.
proof: Proof. intros a b. set (d := (a - b)%Z). replace a with (b + d)%Z; [ idtac | unfold d in |- *; lia ]. case d; simpl in |- *. left; right; auto with zarith. intro p. right. rewrite <- (Zplus_0_r b). replace (b + 0 + Zpos p)%Z with (b + Zpos p)%Z; auto with zarith. intro p. left; left. rewrite <- (Zplus_0_r b). replace (b + 0 + Zneg p)%Z with (b + Zneg p)%Z by auto with zarith. cut (Zneg p < 0)%Z. auto with zarith. apply Zlt_NEG_0. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)