test-suite/micromega/bug_11656.v


1
2
3
4
5
6
7
8
9
10
11

Require Import Lia.
Require Import NArith.
Open Scope N_scope.

Goal forall (a b c: N),
    a <> 0 ->
    c <> 0 ->
    a * ((b + 1) * c) <> 0.
Proof.
  intros. nia.
Qed.