proposition: Lemma abs_pred_pos : forall x : Z, (0 < x)%Z -> pred (Z.abs_nat x) = Z.abs_nat (x - 1).
proof: Proof. intros. rewrite abs_minus_pos. replace (Z.abs_nat 1) with 1. rewrite predminus1. reflexivity. reflexivity. apply Zlt_le_weak. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. apply Z.le_ge. change (Z.succ 0 <= x)%Z in |- *. apply Zlt_le_succ. assumption. Qed.
imports: ZArith EqNat lemmas