proposition: Lemma bin_lt_is_wf : wf_ind Qpositive bin_lt.
proof: Proof. generalize (well_founded_lt_compat Qpositive Qpositive_length bin_lt bin_lt_compat_via_length). intro H. exact (well_founded_ind H). Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)