proposition: Lemma bin_lt_is_transitive : forall x y z : Qpositive, bin_lt x y -> bin_lt y z -> bin_lt x z.
proof: Proof. intros x y z; unfold bin_lt in |- *. apply Nat.lt_trans. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)