Goal forall n m, S n + S m = 0. unfold plus. fold plus. Admitted. Goal forall n m, S n + S m = 0. simpl. Admitted. Definition ifzero (n:nat) := if n then True else False. Goal forall n, ifzero n. (* red. (* usunac *) *) intro. case n. hnf. auto. hnf. (* pod produktem nic nie zrobi *) red. Admitted. Goal 21+23=44. compute. trivial. Qed. Goal forall n m, (3 + n) + S m = 0. compute. Admitted. Goal forall k l , (fun n m => (3 + n) + S m) k l = 0. lazy -[plus]. Admitted. Goal (fun x y => y=y) (30000*2) 7. Time cbv. Admitted. Goal (fun x y => y=y) (30000*2) 7. Time lazy. Admitted. Goal (fun x y => y=y) (30000*2) 7. Time vm_compute. Admitted. Goal (20*30=17 -> 3=4). intro H. compute in H. discriminate H. Qed. Goal 3+0 = 5 -> (1+2) + (1+2) = (1+2). intro. change (1+2) with (2+1). change (2+1) at 1 3 with (3+0). rewrite H. Admitted. Goal forall n:nat, n=n. intro. (* apply nat_ind. (* usunac *) *) Check nat_ind. pattern n at 1. apply nat_ind. Admitted.