(* Zdefiniuj funkcje Fibonacciego 
f_0=1
f_1=1
f_{n+2}=f_n+f_{n+1}

*)

Fixpoint Fib1 (n: nat) : nat := 


(*Teraz zdefiniuj funkcje ktora naraz oblicza f_n i f_{n+1}*)

Print prod.

Fixpoint F2 (n:nat) : nat*nat :=


Definition Fib2 := fun n:nat => fst (F2 n).
    
(*Udowodnij, że Fib1 i Fib2 obliczaja "takie same" wyniki*)

Lemma Fib12 : forall n:nat, Fib1 n = Fib2 n.

    
(*Zdefiniuj funkcje Fibonacciego uzywajac rekursji ogonowej. 
Pokaz ze funkcja ta oblicza takie same wyniki jak Fib1*)