proposition: Lemma Zind_wf_double : forall (P : Z -> Z -> Prop) (p0 q0 : Z), (forall n m : Z, (forall p q : Z, (q0 <= q)%Z -> (p0 <= p < n)%Z -> P p q) -> (forall p : Z, (q0 <= p < m)%Z -> P n p) -> P n m) -> forall p q : Z, (q0 <= q)%Z -> (p0 <= p)%Z -> P p q.
proof: Proof. intros P p0 q0 Hrec p. intros. generalize q H. pattern p in |- *. apply Zind_wf with (p := p0). intros p1 H1. intros. pattern q1 in |- *. apply Zind_wf with (p := q0). intros q2 H3. apply Hrec. intros. apply H1. assumption. assumption. intros. apply H3. assumption. assumption. assumption. Qed.
imports: Coq(Lia)