proposition: Lemma qlt_wf_rec_without_zeros_and_One : forall P : Z -> Z -> Z -> Z -> Qpositive -> Prop, (forall (a b c d : Z_pos) (p : Qpositive), (forall (r s t u : Z_pos) (p1 : Qpositive), qlt r s t u p1 a b c d p -> P r s t u p1) -> P a b c d p) -> forall (a b c d : Z_pos) (p : Qpositive), P a b c d p.
proof: Proof. intros P H (a, Ha) (b, Hb) (c, Hc) (d, Hd) p. set (P2 := fun (p_i : Qpositive) (x : Z4) => P (fst (fst x)) (snd (fst x)) (fst (snd x)) (snd (snd x)) p_i) in *. simpl in |- *. assert (z4prf_Z4 : (0 <= a)%Z /\ (0 <= b)%Z /\ (0 <= c)%Z /\ (0 <= d)%Z); repeat split; try assumption. assert (P2 p (Build_Z4 (a, b, (c, d)) z4prf_Z4)). apply (merge_lt_wf Qpositive_as_well_ordering Z4_as_well_ordering). intro p_i. intros (((a_i, b_i), (c_i, d_i)), q); revert q. unfold P2 in |- *. simpl in |- *. intros (Ha_i, (Hb_i, (Hc_i, Hd_i))). intros. change (P (Build_Z_pos a_i Ha_i) (Build_Z_pos b_i Hb_i) (Build_Z_pos c_i Hc_i) (Build_Z_pos d_i Hd_i) p_i) in |- *. apply H. intros (r_, r_p) (s_, s_p) (t_, t_p) (u_, u_p) p1. simpl in |- *. intro H1. assert (z4prf2_Z4 : (0 <= r_)%Z /\ (0 <= s_)%Z /\ (0 <= t_)%Z /\ (0 <= u_)%Z); repeat split; try assumption. apply (H0 p1 (Build_Z4 (r_, s_, (t_, u_)) z4prf2_Z4)). case H1. intro. left. assumption. intros (H2, H3). right. split; assumption. assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)