Require Bool.

Lemma bool_dec1
     : (b:bool)~(Is_true b)->(Is_true (negb b)).
Induction b.
Simpl.
Intro.
Unfold not  in H.
Apply H.
Try Trivial.

Simpl.
Intro.
Try Trivial.
Save.

Lemma bool_dec2
     : (b:bool)~b=true->(Is_true (negb b)).
Induction b.
Intros.
Apply bool_dec1.
Unfold not  in H.
Unfold not .
Intro.
Apply H.
Try Trivial.

Simpl.
Try Trivial.
Save.

Lemma bool_dec3
     : (b:bool)(Is_true b)->(b=true).
Induction b.
Intro.
Try Trivial.

Intros H.
Inversion H.
Save.

Lemma bool_dec4
     : (b:bool)~b=false->b=true.
Induction b.
Intro.
Try Trivial.

Cut (false = (negb true)).

Intro.
Rewrite -> H.
Intros.
Apply bool_dec3.
Apply bool_dec2.
Unfold not  in H0.
Unfold not .
Intro.
Apply H0.
Try Trivial.

Simpl.
Try Trivial.
Save.

Lemma bool_dec5
     : (b:bool)~b=true->b=false.
Induction b.
Intro.
Cut (Is_true (negb true)).
Simpl.
(Intro;Contradiction).

Apply bool_dec2.
Try Trivial.

Intro.
Try Trivial.
Save.

Lemma bool_dec6
     : (b:bool)b=false->~b=true.
Induction b.
(Intros d;Discriminate d).

Intro.
Discriminate.
Save.

Lemma bool_dec7
     : (b:bool)b=true->~b=false.
Induction b.
Intros.
Discriminate.

(Intros d;Discriminate d).
Save.

Section boolean_extension.

(* Giving if constructor over bool for general sets.*)

Hypothesis genset:Set.
Recursive Definition
    Setifb : bool->genset->genset->genset :=
	true x y => x |
	false x y => y.

Lemma orbor : (b1,b2:bool)
	(orb b1 b2)=true->b1=true\/b2=true.
Intros b1 b2.
Case b1.
Auto.

Case b2.
Auto.

Auto.
Save.

End boolean_extension.

Lemma ororb : (b1,b2:bool)
	(b1=true\/b2=true)->(orb b1 b2)=true.

Intros.
Case H.
Intros.
Rewrite -> H0.
Auto.

Intros.
Rewrite -> H0.
Case b1.
Auto.

Auto.
Save.

Lemma orbor1 :  (b1,b2:bool)
	(orb b1 b2)=false->b1=false/\b2=false.
Intros b1 b2.
Case b1.
Simpl.
(Intros d;Discriminate d).

Simpl.
Auto.

Save.

Lemma ororb1 : (b1,b2:bool)
	(b1=false/\b2=false)->(orb b1 b2)=false.
Intros.
Case H.
Intros.
Rewrite -> H0.
Rewrite -> H1.
Auto.
Save.

Lemma sym_andb : (b1,b2:bool)
	(andb b1 b2)=(andb b2 b1).
Intros.
(Case b1; Case b2; Auto).
Save.

Lemma andbf : (b:bool)
	(andb b false)=false.
Intros.
Rewrite sym_andb; Auto.
Save.