blob: 501fafc0b3d0135442c06b80b2df05b4a98705b1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Require Import ZArith.
Require Import Lia.
Import Z.
Unset Lia Cache.
Goal forall (x y : Z),
implb (Z.eqb x y) (Z.eqb y x) = true.
Proof.
intros.
lia.
Qed.
Goal forall (x y :Z), implb (Z.eqb x 0) (Z.eqb y 0) = true <->
orb (negb (Z.eqb x 0))(Z.eqb y 0) = true.
Proof.
intro.
lia.
Qed.
|
