aweinstock

    $ python
    >>> import z3
    >>> x, y = z3.Ints('x y')
    >>> s = z3.Solver()
    >>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0)))))
    >>> s.check()
    unknown

    $ coqtop
    Require Import NArith.
    Require Import Omega.

    Lemma x_le_fact : forall x, x <= fact x.
    induction x;.
    - simpl; omega.
    - simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *)
    Admitted.

    Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0.
    intros x; exists (fact x).
    split.
    - unfold ">=". apply x_le_fact.
    - induction x.
        + simpl; reflexivity.
        +
      (* goal here is `fact (S x) mod S x = 0` *)
      unfold fact; fold fact.
      (* goal here is `(S x * fact x) mod S x = 0` *)
      rewrite (Nat.mul_comm (S x) (fact x)).
      (* goal here is `(fact x * S x) mod S x = 0` *)
      apply (Nat.mod_mul (fact x) (S x)).
      discriminate.
    Qed.

    int main() {
        char buf[20];
        fgets(buf, sizeof buf, stdin);
        printf(buf);
        return 0;
    }