proposition: Lemma bin2_lt_is_transitive : forall x y z : Qpositive2, bin2_lt x y -> bin2_lt y z -> bin2_lt x z.
proof: Proof. intros (p1_x, p2_x) (p1_y, p2_y) (p1_z, p2_z). unfold bin2_lt in |- *. apply bin_lt_is_transitive. Qed.
imports: QArithSternBrocot(Merge_Order)