fact: Definition quadratic_top_more (a b c d e f g h : Z) := (e <= a)%Z /\ (f <= b)%Z /\ (g <= c)%Z /\ (h < d)%Z \/ (e <= a)%Z /\ (f <= b)%Z /\ (g < c)%Z /\ (h <= d)%Z \/ (e <= a)%Z /\ (f < b)%Z /\ (g <= c)%Z /\ (h <= d)%Z \/ (e < a)%Z /\ (f <= b)%Z /\ (g <= c)%Z /\ (h <= d)%Z.
imports: QArithSternBrocot(Merge_Order)