proposition: Lemma Zind_wf : forall (P : Z -> Prop) (p : Z), (forall q : Z, (forall r : Z, (p <= r < q)%Z -> P r) -> P q) -> forall q : Z, (p <= q)%Z -> P q.
proof: Proof. intros P p WF_ind_step q Hq. cut (forall x : Z, (p <= x)%Z -> forall y : Z, (p <= y < x)%Z -> P y). intro. apply (H (Z.succ q)). apply Zle_le_succ. assumption. split; [ assumption | exact (Zlt_succ q) ]. intros x0 Hx0; generalize Hx0; pattern x0 in |- *. apply Zind with (p := p). intros. absurd (p <= p)%Z. apply Zgt_not_le. apply Zgt_le_trans with (m := y). apply Z.lt_gt. elim H. intros. assumption. elim H. intros. assumption. apply Z.le_refl. intros. apply WF_ind_step. intros. apply (H0 H). split. elim H2. intros. assumption. apply Z.lt_le_trans with y. elim H2. intros. assumption. apply Zgt_succ_le. apply Z.lt_gt. elim H1. intros. unfold Z.succ in |- *. assumption. assumption. Qed.
imports: Coq(Lia)