proposition: Lemma bin_eq_is_transitive : forall x y z : Qpositive, bin_eq x y -> bin_eq y z -> bin_eq x z.
proof: Proof. intros x y z. unfold bin_eq in |- *. apply trans_eq. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)