fact: Definition same_ratio (a b c d e f g h : Z) := (a * f)%Z = (b * e)%Z /\ (b * g)%Z = (c * f)%Z /\ (c * h)%Z = (d * g)%Z /\ (a * g)%Z = (c * e)%Z /\ (a * h)%Z = (d * e)%Z /\ (b * h)%Z = (d * f)%Z.
imports: Coq(ZArithRing)