proposition: Lemma Z8_lt_is_wf : wf_ind Z8 Z8_lt.
proof: Proof. red in |- *. intros P H ((((a, b), (c, d)), ((e, f), (g, h))), p); revert p. simpl in |- *. intros (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh))))))). assert (H_a_b_c_d_e_f_g_h : (0 <= a + b + c + d + e + f + g + h)%Z); repeat apply Zplus_le_0_compat; try assumption. set (P8 := fun k : Z_pos => forall (a b c d e f g h : Z) (Habcdefgh : (0 <= a)%Z /\ (0 <= b)%Z /\ (0 <= c)%Z /\ (0 <= d)%Z /\ (0 <= e)%Z /\ (0 <= f)%Z /\ (0 <= g)%Z /\ (0 <= h)%Z) (Hk : zposcrr k = (a + b + c + d + e + f + g + h)%Z), P (Build_Z8 (a, b, (c, d), (e, f, (g, h))) Habcdefgh)) in *. assert (P8 (Build_Z_pos (a + b + c + d + e + f + g + h) H_a_b_c_d_e_f_g_h)). apply Z_pos_lt_is_wf. intros q_pos. red in |- *. intros. apply H. intros ((((r_a, r_b), (r_c, r_d)), ((r_e, r_f), (r_g, r_h))), p); revert p. simpl in |- *. intros (H_r_a, (H_r_b, (H_r_c, (H_r_d, (H_r_e, (H_r_f, (H_r_g, H_r_h))))))). intro Hr. assert (H_r_a_b_c_d_e_f_g_h : (0 <= r_a + r_b + r_c + r_d + r_e + r_f + r_g + r_h)%Z); repeat apply Zplus_le_0_compat; try assumption. assert (P8 (Build_Z_pos (r_a + r_b + r_c + r_d + r_e + r_f + r_g + r_h) H_r_a_b_c_d_e_f_g_h)). apply H0. rewrite Hk. simpl in |- *. assumption. apply H1. reflexivity. apply H0. reflexivity. Qed.
imports: QArithSternBrocot(Merge_Order)