Require Import Arith.

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


Functional Scheme div2_ind := Induction for div2 Sort Prop.

Print div2_ind.

Lemma div2_le : forall n:nat, div2 n <= n.
intro n.
functional induction (div2 n).
auto with arith.
auto with arith.
auto with arith.
Qed.





Function div22 (n:nat) : nat := 
  match n with
  | O => 0
  | S O => 0
  | S (S n') => S (div22 n')
  end.


Print R_div22.
Check R_div22_complete.

Check R_div22_ind.

Lemma div22_le : forall n:nat, div22 n <= n.
intro n.
functional induction (div22 n).
auto with arith.
auto with arith.
auto with arith.
Qed.