proposition: Lemma bin_eq_is_equality : is_equality Qpositive bin_eq.
proof: Proof. split. apply bin_eq_is_reflexive. split. apply bin_eq_is_symmetric. apply bin_eq_is_transitive. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)