proposition: Lemma Zopp1 : forall n : Z, (n < 0)%Z -> (- n > 0)%Z.
proof: Proof. simple induction n. intros H'; try assumption. inversion H'. intros p H'; try assumption. replace 0%Z with (- (0))%Z. apply Zlt_gt; auto with algebra. auto with algebra. intros p H'; try assumption. replace 0%Z with (- (0))%Z. apply Zlt_gt; auto with algebra. auto with algebra. Qed.
imports: Z_group