proposition: Lemma Zopp_lt_gt_0 : forall x : Z, (x < 0)%Z -> (- x > 0)%Z.
proof: Proof. simple induction x. intro. unfold Z.lt in H. simpl in H. discriminate H. intros. unfold Z.lt in H. simpl in H. discriminate H. intros. simpl in |- *. unfold Z.gt in |- *. simpl in |- *. reflexivity. Qed.
imports: ZArith EqNat