(* typ bool *)

Inductive bool:Set:=true:bool|false:bool.

Definition b_or : bool -> bool -> bool := ...

Definition b_and : bool -> bool -> bool := ...

Definition b_not : bool -> bool := ...

Theorem b_Morgan1 : 
  forall b1 b2:bool, b_not (b_and b1 b2) = b_or (b_not b1) (b_not b2).

Theorem b_Morgan2 : 
  forall b1 b2:bool, b_not (b_or b1 b2) = b_and (b_not b1) (b_not b2).

(* typ nat *)

Definition pred : nat->nat := ...

Print pred.

Lemma pred_S : forall n:nat, pred (S n)=n.

Lemma S_pred : forall n:nat, n=O \/ S(pred n)=n.

(* proste relacje indukcyjne *)

Inductive Even : nat -> Prop :=
   evenO : Even O
 | evenSS : forall n:nat, Even n -> Even (S (S n)).

Lemma SS_Even : forall n:nat, Even n -> Even (S (S n)).

Inductive Ev : nat -> Prop :=
 | evO : Ev O
 | evS : forall n:nat, Odd n -> Ev (S n)
with Odd : nat -> Prop :=
 | oddS : forall n:nat, Ev n -> Odd (S n).

Lemma SS_Odd : forall n:nat, Odd n -> Odd (S (S n)).

Lemma Odd_SS : forall n:nat, Odd n -> Ev (pred n).