proposition: Lemma Zlt_opp : forall x y : Z, (x < y)%Z -> (- x > - y)%Z.
proof: Proof. intros x y H. red in |- *. apply sym_eq. cut (Datatypes.Gt = (y ?= x)%Z). intro H0. cut ((y ?= x)%Z = (- x ?= - y)%Z). intro H1. exact (trans_eq H0 H1). exact (Zcompare_opp y x). apply sym_eq. exact (Z.lt_gt x y H). Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid