coq - `forall n k, (forall q, n <> q * 3) -> n + n <> k * 3` 的简短证明

Question

在证明中，我需要证明“如果 n 不是三的倍数，那么 n+n 也不是三的倍数”。我认为我的证明太长而且不是很优雅。有没有更漂亮的写法？有没有ssreflect？ (我确定 ssreflect 中有一个 oneliner :))。

我的证明对 n 做了归纳分三步。

Require Import Omega.
Lemma math_helper n: forall k, (forall q, n <> q * 3) ->  n + n <> k * 3.
  (* name the predicate Q and strengthen induction hypothesis *)
  pattern n; match goal with [ _:_ |- ?P ?n] => let X := fresh Q in remember P as X end.
  enough (Q n /\ Q (1+n) /\ Q (2+n)) by tauto.
  induction n; subst Q;
    [| destruct IHn as [IH1 [IH2 IH3]]];
    repeat split; simpl; intros; auto; try omega.
  intro C; assert (k>=2) by omega; do 2 (try destruct k); try omega.
  assert (n+n = k*3) by omega.
  apply (IH1 k); auto; intros q HH; eapply (H (1+q)); subst n; omega.
Qed.

Answer 1

还有一个更简单的解决方案，就是依靠除法，让欧米茄来推理。

Lemma math_helper2 n : forall k, (forall q, n <> q * 3) ->  n + n <> k * 3.
Proof.
intros k kq A.
assert (k = 2 * (k / 2) + k mod 2) by (apply Nat.div_mod; omega).
assert (k mod 2 < 2) by (apply (Nat.mod_bound_pos k 2); omega).
apply (kq (k/2)); omega.
Qed.