proposition: Lemma same_ratio_dec_inf : forall a b c d e f g h : Z, {same_ratio a b c d e f g h} + {~ same_ratio a b c d e f g h}.
proof: Proof. intros. case (Z.eq_dec (a * f) (b * e)); [ case (Z.eq_dec (b * g) (c * f)); [ case (Z.eq_dec (c * h) (d * g)); [ case (Z.eq_dec (a * g) (c * e)); [ case (Z.eq_dec (a * h) (d * e)); [ case (Z.eq_dec (b * h) (d * f)); [ left; repeat split; assumption | idtac ] | idtac ] | idtac ] | idtac ] | idtac ] | idtac ]; intro H'; try intros; right; intros (Hafbe, (Hbgcf, (Hchgd, (Hagce, (Hahde, Hbhdf))))); apply H'; assumption. Qed.
imports: Coq(ZArithRing)