proposition: Theorem Zminus2_wf : forall x y : Z, (0%nat < x)%Z -> (0 < y)%Z -> fractionalAcc x y.
proof: Proof. intros x y. case (Z_lt_le_dec 0 x). intro H. case (Z_lt_le_dec 0 y). intro H2. apply Zind_wf_double with (P := fun x y : Z => (0 < x)%Z -> (0 < y)%Z -> fractionalAcc x y) (p0 := 1%Z) (q0 := 1%Z). intros. case (Z.eq_dec n m). intro. apply fractionalacc0. assumption. intro H5. case (not_Zeq_inf n m H5). intro. apply fractionalacc1. assumption. assumption. apply H1. split. apply Zplus_le_reg_l with n. replace (n + (m - n))%Z with m. change (Z.succ n <= m)%Z in |- *. apply Zlt_le_succ. assumption. ring. apply Zplus_lt_reg_l with (n - m)%Z. replace (n - m + (m - n))%Z with 0%Z. replace (n - m + m)%Z with n. assumption. ring. ring. assumption. unfold Zminus in |- *. apply Zlt_left_lt. assumption. intro. apply fractionalacc2. assumption. assumption. apply H0. change (Z.succ 0 <= m)%Z in |- *. apply Zlt_le_succ. assumption. split. apply Zplus_le_reg_l with m. replace (m + (n - m))%Z with n. change (Z.succ m <= n)%Z in |- *. apply Zlt_le_succ. assumption. ring. apply Zplus_lt_reg_l with (m - n)%Z. replace (m - n + (n - m))%Z with 0%Z. replace (m - n + n)%Z with m. assumption. ring. ring. unfold Zminus in |- *. apply Zlt_left_lt. assumption. assumption. change (Z.succ 0 <= y)%Z in |- *. apply Zlt_le_succ. assumption. change (Z.succ 0 <= x)%Z in |- *. apply Zlt_le_succ. assumption. intros. absurd (y <= 0)%Z. apply Zgt_not_le. Flip. assumption. intros. absurd (x <= 0)%Z. apply Zgt_not_le. Flip. assumption. Defined.
imports: Coq(ZArithRing) Coq(FunInd)