proposition: Theorem lt_mult_conv : forall x y z : nat, S x * y < S x * z -> y < z.
proof: Proof. intros x y z. elim (Nat.le_gt_cases z y). intros H; generalize ((fun m n p : nat => Nat.mul_le_mono_l p n m) (S x) _ _ H). intros H1 H2; apply Nat.le_ngt in H1; contradict H1; auto. auto. Qed.