fact: Definition octet_lt (a b c d e f g h : Z) (p1 p2 : Qpositive) (a' b' c' d' e' f' g' h' : Z) (p1' p2' : Qpositive) : Prop := bin_lt p1 p1' \/ p1 = p1' /\ (a + b + c + d + e + f + g + h < a' + b' + c' + d' + e' + f' + g' + h')%Z.
imports: QArithSternBrocot(Merge_Order)