proposition: Lemma Z_pos_lt_is_wf : forall P : Z_pos -> Prop, (forall q : Z_pos, (forall r : Z_pos, (r < q)%Z -> P r) -> P q) -> forall q : Z_pos, P q.
proof: Proof. intros. destruct q. rename zposcrr0 into q. set (P2 := fun p : Z => forall Hp : (0 <= p)%Z, P (Build_Z_pos p Hp)) in *. assert (P2 q). apply Zind_wf with (p := 0%Z). intros. unfold P2 in |- *. intro. apply H. intros. destruct r. rename zposcrr0 into r. assert (P2 r). apply H0. split. assumption. assumption. apply (H2 z4prf_Z_pos1). assumption. apply (H0 z4prf_Z_pos0). Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)