proposition: Lemma Zlemma1 : forall x : Z, (x < 0)%Z -> (- x > 0)%Z.
proof: Proof. intros x H'; try assumption. apply Zlt_gt. replace (- x)%Z with (- x + 0)%Z. pattern 0%Z at 1 in |- *. replace 0%Z with (- x + x)%Z. apply Zlt_reg_l. auto with *. apply Zplus_opp_l. apply Zplus_0_r. Qed.
imports: Zring Group_kernel