(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(* ---                        matrix.v                                  --- *)
(*                                                                          *)
(* Author: Pierre Casteran.                                                 *)
(*    LABRI, URA CNRS 1304,                                                 *)
(*    Departement d'Informatique, Universite Bordeaux I,                    *)
(*    33405 Talence CEDEX,                                                  *)
(*    e-mail:  casteran@labri.u-bordeaux.fr                                 *)

(*          2-2 matrices with natural coefficients                          *)

(* Ported to ZArith by P.Letouzey (nov 2001)                                *)

Require Import monoid.
Require Import Arith.
Require Import ZArith.
Require Import Compare_dec.
Require Import fmpc.

Record Mat2 : Set := mat2 {M11 : Z; M12 : Z; M21 : Z; M22 : Z}.

Definition Id2 := mat2 1 0 0 1.   

Definition Mat_mult (M M' : Mat2) :=
  mat2 (M11 M * M11 M' + M12 M * M21 M') (M11 M * M12 M' + M12 M * M22 M')
    (M21 M * M11 M' + M22 M * M21 M') (M21 M * M12 M' + M22 M * M22 M').


Axiom
  Mat_assoc :
    forall M M' M'' : Mat2,
    Mat_mult M (Mat_mult M' M'') = Mat_mult (Mat_mult M M') M''.


Lemma matrix : monoid Mat2.
(* Goal: monoid Mat2 *)
 refine (mkmonoid Mat2 Id2 Mat_mult _ _ _).
(*
 Realizer (mkmonoid Mat2 Id2 Mat_mult).
 Program_all.
*)
(* Goal: forall a b c : Mat2, @eq Mat2 (Mat_mult a (Mat_mult b c)) (Mat_mult (Mat_mult a b) c) *)
(* Goal: forall a : Mat2, @eq Mat2 (Mat_mult Id2 a) a *)
(* Goal: forall a : Mat2, @eq Mat2 (Mat_mult a Id2) a *)
 exact Mat_assoc.
(* Goal: forall a : Mat2, @eq Mat2 (Mat_mult a Id2) a *)
 simple induction a. 
(* Goal: forall M11 M12 M21 M22 : Z, @eq Mat2 (Mat_mult Id2 (mat2 M11 M12 M21 M22)) (mat2 M11 M12 M21 M22) *)
(* Goal: forall a : Mat2, @eq Mat2 (Mat_mult a Id2) a *)
  intros M13 M14 M23 M24.
(* Goal: @eq Mat2 (Mat_mult (mat2 M13 M14 M23 M24) Id2) (mat2 M13 M14 M23 M24) *)
  unfold Id2, Mat_mult in |- *; simpl in |- *.
(* Goal: @eq Mat2 (mat2 (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match d with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end Z0) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end Z0)) (mat2 (Z.add a b) (Z.add b d) a b) *)
  repeat elim Zplus_0_r_reverse.
(* Goal: @eq Mat2 (mat2 match M13 with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match M14 with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match M23 with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match M24 with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (mat2 M13 M14 M23 M24) *)
(* Goal: forall a : Mat2, @eq Mat2 (Mat_mult a Id2) a *)
  case M13; case M14; case M23; case M24; auto.
(* Goal: forall a : Mat2, @eq Mat2 (Mat_mult a Id2) a *)
  simple induction a. 
(* Goal: forall (n : nat) (_ : forall _ : lt O n, @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n))) (_ : lt O (S n)), @eq Z (Z.of_nat (Fib (S n))) (M11 (power Mat2 matrix fib_mat (S n))) *)
  intros.
(* Goal: @eq Mat2 (Mat_mult (mat2 M13 M14 M23 M24) Id2) (mat2 M13 M14 M23 M24) *)
  unfold Id2, Mat_mult in |- *; simpl in |- *.
(* Goal: @eq Mat2 (mat2 (Z.add (Z.mul M13 (Zpos xH)) (Z.mul M14 Z0)) (Z.add (Z.mul M13 Z0) (Z.mul M14 (Zpos xH))) (Z.add (Z.mul M23 (Zpos xH)) (Z.mul M24 Z0)) (Z.add (Z.mul M23 Z0) (Z.mul M24 (Zpos xH)))) (mat2 M13 M14 M23 M24) *)
  repeat elim Zmult_0_r_reverse.
(* Goal: @eq Mat2 (mat2 (Z.add (Z.mul M13 (Zpos xH)) Z0) (Z.add Z0 (Z.mul M14 (Zpos xH))) (Z.add (Z.mul M23 (Zpos xH)) Z0) (Z.add Z0 (Z.mul M24 (Zpos xH)))) (mat2 M13 M14 M23 M24) *)
  repeat rewrite Zmult_1_r. 
(* Goal: @eq Mat2 (mat2 (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match d with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end Z0) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end Z0)) (mat2 (Z.add a b) (Z.add b d) a b) *)
  simpl in |- *; repeat elim Zplus_0_r_reverse.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
  auto with arith.
Defined.

(* Fibonacci numbers *)

(* definition *)

Fixpoint Fib (n : nat) : nat :=
  match n return nat with
  | O => (* O *)  1
      (* (S p ) *) 
  | S p =>
      match p return nat with
      | O => (* O *)  1
          (* S q *)
      | S q => Fib q + Fib p
      end
  end.

Lemma Unfold_FibO : Fib 0 = 1.
Proof.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 unfold Fib in |- *; simpl in |- *; auto with arith.
Qed.

Lemma Unfold_Fib1 : Fib 1 = 1.
Proof.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 unfold Fib in |- *; simpl in |- *; auto with arith.
Qed.

Lemma Unfold_FibSSn : forall n : nat, Fib (S (S n)) = Fib (S n) + Fib n.
Proof.
(* Goal: forall n : nat, @eq nat (Fib (S (S n))) (Init.Nat.add (Fib (S n)) (Fib n)) *)
 intro n; unfold Fib at 1 in |- *.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 simpl in |- *; auto with arith.
Qed.


(* A "Decaled" Fibonnacci function *)

Definition shift_Fib (n : nat) :=
  match n return nat with
  | O => 0
  | S p => Fib p
  end.

Lemma Unfold_shift_Fib : forall n : nat, shift_Fib (S n) = Fib n.
Proof.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 intro n; unfold shift_Fib in |- *; auto with arith.
Qed.

Lemma Simpl_shift_Fib :
 forall n : nat, shift_Fib (S (S n)) = shift_Fib (S n) + shift_Fib n.
Proof.
(* Goal: forall (n : nat) (_ : lt O n), @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n)) *)
 simple induction n.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 unfold shift_Fib, Fib in |- *; simpl in |- *; auto with arith.
(* Goal: forall (n : nat) (_ : forall _ : lt O n, @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n))) (_ : lt O (S n)), @eq Z (Z.of_nat (Fib (S n))) (M11 (power Mat2 matrix fib_mat (S n))) *)
 intros.
(* Goal: @eq nat (shift_Fib (S (S (S n0)))) (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0))) *)
 unfold shift_Fib in |- *.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 rewrite Unfold_FibSSn; auto with arith.
Qed.


Definition fib_mat := mat2 1 1 1 0.


Lemma fib_mat_n :
 forall (n : nat) (a b d : Z),
 power Mat2 matrix fib_mat n = mat2 a b b d ->
 power Mat2 matrix fib_mat (S n) = mat2 (a + b) (b + d) a b.
Proof.
(* Goal: forall (n : nat) (a b d : Z) (_ : @eq Mat2 (power Mat2 matrix fib_mat n) (mat2 a b b d)), @eq Mat2 (power Mat2 matrix fib_mat (S n)) (mat2 (Z.add a b) (Z.add b d) a b) *)
 intros; simpl in |- *.
(* Goal: @eq Mat2 (Mat_mult fib_mat (power Mat2 matrix fib_mat n)) (mat2 (Z.add a b) (Z.add b d) a b) *)
 rewrite H.
(* Goal: @eq Mat2 (Mat_mult fib_mat (mat2 a b b d)) (mat2 (Z.add a b) (Z.add b d) a b) *)
 unfold Mat_mult in |- *.
(* Goal: @eq Mat2 (mat2 (Z.add (Z.mul (M11 fib_mat) (M11 (mat2 a b b d))) (Z.mul (M12 fib_mat) (M21 (mat2 a b b d)))) (Z.add (Z.mul (M11 fib_mat) (M12 (mat2 a b b d))) (Z.mul (M12 fib_mat) (M22 (mat2 a b b d)))) (Z.add (Z.mul (M21 fib_mat) (M11 (mat2 a b b d))) (Z.mul (M22 fib_mat) (M21 (mat2 a b b d)))) (Z.add (Z.mul (M21 fib_mat) (M12 (mat2 a b b d))) (Z.mul (M22 fib_mat) (M22 (mat2 a b b d))))) (mat2 (Z.add a b) (Z.add b d) a b) *)
 simpl in |- *.
(* Goal: @eq Mat2 (mat2 (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match d with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end Z0) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end Z0)) (mat2 (Z.add a b) (Z.add b d) a b) *)
 repeat elim Zplus_0_r_reverse.
(* Goal: @eq Mat2 (mat2 (Z.add match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (Z.add match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match d with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) match a with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end match b with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (mat2 (Z.add a b) (Z.add b d) a b) *)
 case a; case b; case d; auto.
Qed.

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.
(* Goal: forall (n : nat) (_ : lt O n), @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n)) *)
 simple induction n.
(* Goal: @eq Mat2 (mat2 (Z.add (Z.mul (M11 fib_mat) (M11 (mat2 a b b d))) (Z.mul (M12 fib_mat) (M21 (mat2 a b b d)))) (Z.add (Z.mul (M11 fib_mat) (M12 (mat2 a b b d))) (Z.mul (M12 fib_mat) (M22 (mat2 a b b d)))) (Z.add (Z.mul (M21 fib_mat) (M11 (mat2 a b b d))) (Z.mul (M22 fib_mat) (M21 (mat2 a b b d)))) (Z.add (Z.mul (M21 fib_mat) (M12 (mat2 a b b d))) (Z.mul (M22 fib_mat) (M22 (mat2 a b b d))))) (mat2 (Z.add a b) (Z.add b d) a b) *)
 unfold power, shift_Fib, o, u in |- *; simpl in |- *.
(* Goal: @eq Mat2 (mat2 (Z.add (Z.mul (M11 fib_mat) (M11 (mat2 a b b d))) (Z.mul (M12 fib_mat) (M21 (mat2 a b b d)))) (Z.add (Z.mul (M11 fib_mat) (M12 (mat2 a b b d))) (Z.mul (M12 fib_mat) (M22 (mat2 a b b d)))) (Z.add (Z.mul (M21 fib_mat) (M11 (mat2 a b b d))) (Z.mul (M22 fib_mat) (M21 (mat2 a b b d)))) (Z.add (Z.mul (M21 fib_mat) (M12 (mat2 a b b d))) (Z.mul (M22 fib_mat) (M22 (mat2 a b b d))))) (mat2 (Z.add a b) (Z.add b d) a b) *)
 unfold fib_mat in |- *; simpl in |- *.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 unfold Mat_mult, Id2 in |- *; simpl in |- *; auto with arith.
(* Goal: forall (n : nat) (_ : forall _ : lt O n, @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n))) (_ : lt O (S n)), @eq Z (Z.of_nat (Fib (S n))) (M11 (power Mat2 matrix fib_mat (S n))) *)
 intros.
(* Goal: @eq Mat2 (power Mat2 matrix fib_mat (S (S n0))) (mat2 (Z.of_nat (shift_Fib (S (S (S n0))))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 rewrite (fib_mat_n (S n0) _ _ _ H).
(* Goal: @eq Mat2 (mat2 (Z.add (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (Z.add (Z.of_nat (shift_Fib (S n0))) (Z.of_nat (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (shift_Fib (S (S (S n0))))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 repeat rewrite <- Znat.inj_plus.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (shift_Fib (S (S (S n0))))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 rewrite (Simpl_shift_Fib (S n0)).
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 pattern (shift_Fib (S (S n0))) at 4 in |- *.
(* Goal: (fun n : nat => @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat n) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0))))) (shift_Fib (S (S n0))) *)
 rewrite (Simpl_shift_Fib n0).
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 auto with arith.
Qed.


Lemma fib_computation :
 forall n : nat,
 0 < n -> Z_of_nat (Fib n) = M11 (power Mat2 matrix fib_mat n).
Proof.
(* Goal: forall (n : nat) (_ : lt O n), @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n)) *)
 simple induction n.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 intro; absurd (0 < 0); auto with arith.
(* Goal: forall (n : nat) (_ : forall _ : lt O n, @eq Z (Z.of_nat (Fib n)) (M11 (power Mat2 matrix fib_mat n))) (_ : lt O (S n)), @eq Z (Z.of_nat (Fib (S n))) (M11 (power Mat2 matrix fib_mat (S n))) *)
 intros.
(* Goal: @eq Mat2 (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) (mat2 (Z.of_nat (Init.Nat.add (shift_Fib (S (S n0))) (shift_Fib (S n0)))) (Z.of_nat (Init.Nat.add (shift_Fib (S n0)) (shift_Fib n0))) (Z.of_nat (shift_Fib (S (S n0)))) (Z.of_nat (shift_Fib (S n0)))) *)
 rewrite fib_n; unfold M11 in |- *; auto with arith.
Qed.