proposition: Lemma bin2_lt_is_wf : wf_ind Qpositive2 bin2_lt.
proof: Proof. red in |- *. intros P H (q1, q2). set (P2 := fun p1 : Qpositive => forall p2 : Qpositive, P (p1, p2)) in *. generalize q2. change (P2 q1) in |- *. apply bin_lt_is_wf. intros. unfold P2 in |- *. intro. apply H. intros (r1, r2). intro. generalize r2. change (P2 r1) in |- *. apply H0. unfold bin2_lt in H1. assumption. Qed.
imports: QArithSternBrocot(Merge_Order)