proposition: Lemma octet_lt_wf_rec_without_zeros_and_One : forall P : Z -> Z -> Z -> Z -> Z -> Z -> Z -> Z -> Qpositive -> Qpositive -> Prop, (forall (a b c d e f g h : Z_pos) (q1 q2 : Qpositive), (forall (k l r s t u v w : Z_pos) (p1 p2 : Qpositive), octet_lt k l r s t u v w p1 p2 a b c d e f g h q1 q2 -> P k l r s t u v w p1 p2) -> P a b c d e f g h q1 q2) -> forall (a b c d e f g h : Z_pos) (q1 q2 : Qpositive), P a b c d e f g h q1 q2.
proof: Proof. intros P H (a, Ha) (b, Hb) (c, Hc) (d, Hd) (e, He) ( f, Hf) (g, Hg) (h, Hh) q1 q2. set (P2 := fun (p_i : Qpositive2) (x : Z8) => P (fst (fst (fst x))) (snd (fst (fst x))) (fst (snd (fst x))) (snd (snd (fst x))) (fst (fst (snd x))) (snd (fst (snd x))) (fst (snd (snd x))) (snd (snd (snd x))) (fst p_i) (snd p_i)) in *. simpl in |- *. assert (z8prf_Z8 : (0 <= a)%Z /\ (0 <= b)%Z /\ (0 <= c)%Z /\ (0 <= d)%Z /\ (0 <= e)%Z /\ (0 <= f)%Z /\ (0 <= g)%Z /\ (0 <= h)%Z); repeat split; try assumption. assert (P2 (q1, q2) (Build_Z8 (a, b, (c, d), (e, f, (g, h))) z8prf_Z8)). apply (merge_lt_wf Qpositive2_as_well_ordering Z8_as_well_ordering). intros (p1_i, p2_i). intros ((((a_i, b_i), (c_i, d_i)), ((e_i, f_i), (g_i, h_i))), p); revert p. unfold P2 in |- *. simpl in |- *. intros (Ha_i, (Hb_i, (Hc_i, (Hd_i, (He_i, (Hf_i, (Hg_i, Hh_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) (Build_Z_pos e_i He_i) (Build_Z_pos f_i Hf_i) (Build_Z_pos g_i Hg_i) (Build_Z_pos h_i Hh_i) p1_i p2_i) in |- *. apply H. intros (k_, k_p) (l_, l_p) (r_, r_p) (s_, s_p) (t_, t_p) ( u_, u_p) (v_, v_p) (w_, w_p) p1 p2. simpl in |- *. intro H1. assert (z8prf2_Z8 : (0 <= k_)%Z /\ (0 <= l_)%Z /\ (0 <= r_)%Z /\ (0 <= s_)%Z /\ (0 <= t_)%Z /\ (0 <= u_)%Z /\ (0 <= v_)%Z /\ (0 <= w_)%Z); repeat split; try assumption. apply (H0 (p1, p2) (Build_Z8 (k_, l_, (r_, s_), (t_, u_, (v_, w_))) z8prf2_Z8)). case H1. intro. left. assumption. intros (H2, H3). right. split; assumption. assumption. Qed.
imports: QArithSternBrocot(Merge_Order)