(* Rownosc *)

Print eq.

(* x=x dla x:A to skrot od (eq A x x) *)

(* Dowodzenie rownosci . *)

Lemma re : (A:Set)(x:A)x=x.

Lemma true_albo_false : (b:bool)(b=true)\/(b=false).


(* Uzywanie rownosci *)

Lemma Leibniz : (A:Set)(x,y:A) x=y -> (P:A->Prop) (P x) -> (P y).

Lemma eq_trans: (A:Set; x,y,z:A)x=y->y=z->x=z.

Lemma f_funkcja : (A,B:Set)(f:A->B)(x,y:A) x=y -> (f x)=(f y).

Print Leibniz.

(* Jak sie typuje ten case ? *)

(* Wezmy najpierw prostszy przyklad: *)

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

Lemma Even_pred_pred : (n:nat)(Even n) -> (Even (pred (pred n))).

(* Jak sie typuje ten cases ? *)
(* Ten od rownosci typuje sie tak samo ! *)


(**********************************************************)

(* Cases zalezny *)
Lemma zero_lub_nie_zero : (n:nat)(n=O \/ n=(S (pred n))).

Show Proof.
(* Jak sie typuje ten cases ? *)

(* napisac _recznie_ stala *)

Definition nat_case 
  : (P:nat -> Prop)(P O) -> ((n:nat)(P (S n))) -> (n:nat)(P n) :=

(**********************************************************)

(* Definicje przez punkt staly *)

Fixpoint plus [n:nat] : nat -> nat :=
 [m:nat]Cases n of
          O   => m
        | (S p) => (S (plus p m)) 
        end.


(* zdefiniuj mnozenie *)

Fixpoint razy [n:nat] : nat -> nat :=


(* zdefiniowac recznie zasade indukcji: *)
(* uzywajac 
(*
nat_rec
     : (P:(nat->Set))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n) 
*)
Fixpoint nat_rec [P:(nat->Set); o:(P O); s:((n:nat)(P n)->(P (S n))); n:nat] 
                                                                 : (P n) := 


(* dowody przez indukcje *)

Lemma plus_zero : (n:nat)(plus n O)=n.

Lemma plus_przem : (n,m:nat)(plus n m) = (plus m n).