(* Udowodnij, ze majac do dyspozycji znaczki o wartosciach 
3 i 5, mozna uzyskac dowolnz sume wieksze rowna 8 *)


Require Import Omega.

Inductive DaSie: nat ->Prop :=
| trzy : DaSie(3)
| piec : DaSie(5)
| plus3: forall (n:nat), DaSie(n) -> DaSie(S(S(S(n))))
| plus5: forall (n:nat), DaSie(n) -> DaSie(S(S(S(S(S(n)))))).

Hint Constructors DaSie.