proposition: Lemma gtzgt : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (x > y)%Z -> Z.abs_nat x > Z.abs_nat y.
proof: Proof. intros. elim (le_or_lt (Z.abs_nat x) (Z.abs_nat y)). intros. elim (Zle_not_lt x y). rewrite <- (inj_abs_pos x). rewrite <- (inj_abs_pos y). apply Znat.inj_le. assumption. apply Z.le_ge. assumption. apply Z.le_ge. assumption. apply Z.gt_lt. assumption. unfold gt in |- *. intro. assumption. Qed.
imports: ZArith EqNat lemmas