proposition: Lemma bin2_lt_is_well_def_rht : is_well_def_rht Qpositive2 bin2_lt bin2_eq.
proof: Proof. red in |- *. intros (p1_x, p2_x) (p1_y, p2_y). intros H (p1_z, p2_z) H0. red in H0. rewrite <- H0. assumption. Qed.
imports: QArithSternBrocot(Merge_Order)