proposition: Lemma Z4_lt_is_wf : wf_ind Z4 Z4_lt.
proof: Proof. red in |- *. intros P H (((a, b), (c, d)), p); revert p; simpl in |- *. intros (Ha, (Hb, (Hc, Hd))). assert (H_a_b_c_d : (0 <= a + b + c + d)%Z); repeat apply Zplus_le_0_compat; try assumption. set (P4 := fun k : Z_pos => forall (a b c d : Z) (Habcd : (0 <= a)%Z /\ (0 <= b)%Z /\ (0 <= c)%Z /\ (0 <= d)%Z) (Hk : zposcrr k = (a + b + c + d)%Z), P (Build_Z4 (a, b, (c, d)) Habcd)) in *. assert (P4 (Build_Z_pos (a + b + c + d) H_a_b_c_d)). apply Z_pos_lt_is_wf. intros q_pos. red in |- *. intros. apply H. intros (((r_a, r_b), (r_c, r_d)), p); revert p. simpl in |- *. intros (H_r_a, (H_r_b, (H_r_c, H_r_d))). intro Hq. assert (H_r_a_b_c_d : (0 <= r_a + r_b + r_c + r_d)%Z); repeat apply Zplus_le_0_compat; try assumption. assert (P4 (Build_Z_pos (r_a + r_b + r_c + r_d) H_r_a_b_c_d)). apply H0. rewrite Hk. simpl in |- *. assumption. apply H1. reflexivity. apply H0. reflexivity. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)