blob: 07cebc8f81578e265983a77fe73c1426cb2b4f97 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import Coq.ZArith.ZArith Coq.omega.Omega.
Local Open Scope Z_scope.
Module Z.
Ltac divide_exists_mul := let k := fresh "k" in
match goal with
| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H;
match type of H with
| ex _ => destruct H as [k H]
| _ => destruct H
end
| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
end; (omega || auto).
End Z.
|
