proposition: Lemma fib_rect : forall P:nat -> Type, P 0 -> P 1 -> (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n:nat, P n.
proof: Proof. intros P H0 H1 HSSn n. assert (X: P n * P (S n)). - induction n as [ | n IHn]. + split; auto. + destruct IHn; split; auto. - now destruct X. Qed.
imports: Arith