proposition: Lemma Zgt_not_eq : forall x y : Z, (x > y)%Z -> x <> y.
proof: Proof. intros x y H. cut (y < x)%Z. intro H0. cut (y <> x). intro H1. red in |- *. intro H2. cut (y = x). intro H3. apply H1. assumption. exact (sym_eq H2). exact (Zorder.Zlt_not_eq y x H0). exact (Z.gt_lt x y H). Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid