proposition: Lemma fib_n : forall n : nat, power Mat2 matrix fib_mat (S n) = mat2 (Z_of_nat (shift_Fib (S (S n)))) (Z_of_nat (shift_Fib (S n))) (Z_of_nat (shift_Fib (S n))) (Z_of_nat (shift_Fib n)).
proof: Proof. simple induction n. unfold power, shift_Fib, o, u in |- *; simpl in |- *. unfold fib_mat in |- *; simpl in |- *. unfold Mat_mult, Id2 in |- *; simpl in |- *; auto with arith. intros. rewrite (fib_mat_n (S n0) _ _ _ H). repeat rewrite <- Znat.inj_plus. rewrite (Simpl_shift_Fib (S n0)). pattern (shift_Fib (S (S n0))) at 4 in |- *. rewrite (Simpl_shift_Fib n0). auto with arith. Qed.
imports: monoid Arith ZArith Compare_dec fmpc