proposition: Lemma Simpl_shift_Fib : forall n : nat, shift_Fib (S (S n)) = shift_Fib (S n) + shift_Fib n.
proof: Proof. simple induction n. unfold shift_Fib, Fib in |- *; simpl in |- *; auto with arith. intros. unfold shift_Fib in |- *. rewrite Unfold_FibSSn; auto with arith. Qed.
imports: monoid Arith ZArith Compare_dec fmpc