(* 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').
(* Goal: 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 |- *.
(* Goal: Included U (fun x : U => and (In U A x) (not (In U B x))) (fun x : U => and (In U A x) (not (In U B' x))) *)
red in |- *; intros x x_in_B.
(* Goal: In U (fun x : U => and (In U A x) (not (In U B' x))) x *)
elim x_in_B; intros x_in_A x_in_nonB.
(* Goal: In U (fun x : U => and (In U A x) (not (In U B' x))) x *)
split.
(* Goal: In U B' x *)
  assumption.
(* Goal: not (In U B' x) *)
red in |- *; intro x_in_B'.
(* Goal: False *)
apply x_in_nonB.
(* Goal: In U B x *)
apply B'_Included_B.
(* Goal: In U B' x *)
assumption.
Qed.

End Contravariance_of_Setminus.


(* $Id$ *)
