proposition: Lemma Zind_wf2 : forall (q : Z) (P : Z -> Prop) (p : Z), (forall q : Z, (forall r : Z, (p <= r < q)%Z -> P r) -> P q) -> (p <= q)%Z -> P q.
proof: Proof. intros. apply Zind_wf with (p := p). assumption. assumption. Qed.
imports: Coq(Lia)