proposition: Lemma Zgt_not_eq : forall x y : Z, (x > y)%Z -> x <> y.
proof: Proof. intros. cut (y < x)%Z. intro. cut (y <> x). intro. red in |- *. intros. cut (y = x). intros. 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)