proposition: Lemma fib_mat_n : forall (n : nat) (a b d : nat), 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: Proof. intros; simpl in |- *. rewrite H. unfold Mat_mult in |- *. simpl in |- *. repeat rewrite plus_0_r. case a; case b; case d; auto. Qed.
imports: monoid Arith Compare_dec fmpc