blob: b06ae922b89a3d7b8c765c731c6769a4f729394e (
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
27
28
29
30
|
Require Import Arith.
Function div2 (n : nat) {struct n}: nat :=
match n with
| 0 => 0
| 1 => 0
| S (S n') => S (div2 n')
end.
Module toto.
Lemma l1: forall n:nat, n = n.
toto.
Qed.
Lemma l2: forall n:nat, n = n.
toto. Qed.
Lemma l3: forall n:nat, n <= n. intro. Qed.
Lemma l4: forall n:nat, n <= n. Proof. intro. Qed.
Lemma l5 : forall n:nat, n <= n.
Proof. intro.
Qed.
Lemma l6: forall n:nat, n = n.
toto.
Lemma l7: forall n:nat, n = n.
toto.
Qed.
Qed.
End toto.
|
