proposition: Theorem lt_mult_right_anti : forall x y z : nat, z * x < z * y -> x < y.
proof: Proof. intros x y z H0; case (Nat.le_gt_cases y x); auto; intros H1. contradict H0; auto; apply Nat.le_ngt; auto with arith. Qed.
imports: Coq(Arith ArithRing)