-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSetminus_fact.v
44 lines (37 loc) · 1.98 KB
/
Setminus_fact.v
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
(* Contribution to the Coq Library V6.3 (July 1999) *)
(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet Coq *)
(* *)
(* INRIA ENS-CNRS *)
(* Rocquencourt Lyon *)
(* *)
(* Coq V5.11 *)
(* Feb 2nd 1996 *)
(* *)
(* (notations and layout updated March 2009) *)
(****************************************************************************)
(* Setminus_fact.v *)
(****************************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(****************************************************************************)
Require Import Ensembles. (* Ensemble, In, Included, Setminus *)
Section Contravariance_of_Setminus.
Variable U : Type.
Lemma Setminus_contravariant :
forall A B B' : Ensemble U,
Included U B' B -> Included U (Setminus U A B) (Setminus U A B').
intros A B B' B'_Included_B; unfold Setminus in |- *.
red in |- *; intros x x_in_B.
elim x_in_B; intros x_in_A x_in_nonB.
split.
assumption.
red in |- *; intro x_in_B'.
apply x_in_nonB.
apply B'_Included_B.
assumption.
Qed.
End Contravariance_of_Setminus.
(* $Id$ *)