# Proofs using specific induction principles

Here is a function of division by 2:

Fixpoint div2 (n:nat):nat:=
match n with 0 => 0 | 1 => 0 | S (S p) => S (div2 p) end.

Define a similar function to compute division by 3, construct a specific induction principle to reason on this function, and use it to show that the result of division is always smaller than the argument.

Define a function rem2 similar to div2, but to compute the remainder of division by 2, use the specific induction principle associated to these function to prove the following statement:

forall n:nat, 2 * div2 n + rem2 n = n

Here are two definitions of the fibonacci function. Using a specific induction principle for the first fibonacci function, prove that the two functions return consistent values.

Fixpoint fib (n:nat) : nat :=
match n with
0 => 1
| 1 => 1
| S ((S p) as q) => fib p + fib q
end.

Fixpoint fib2 (n:nat) : nat*nat :=
match n with
0 => (1, 1)
| S p =>
let (v1, v2) := fib2 p in (v2, v1 + v2)
end.

## Solution

Look at this file

Going home
Pierre Castéran