blob: 24634bd32138bb4f5cacb176ed79a3e6533510db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(* Cf BZ#546 *)
Require Import Lia.
Section S.
Variables n m : nat.
Variable H : n<m.
Inductive Dummy : nat -> Set :=
| Dummy0 : Dummy 0
| Dummy2 : Dummy 2
| DummyApp : forall i j, Dummy i -> Dummy j -> Dummy (i+j).
Definition Bug : Dummy (2*n).
Proof.
induction n.
simpl ; apply Dummy0.
replace (2 * S n0) with (2*n0 + 2) ; auto with arith.
apply DummyApp.
2:exact Dummy2.
apply IHn0 ; abstract lia.
Defined.
End S.
|
