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