proposition: Lemma fib_computation : forall n : nat, 0 < n -> Fib n = M11 (power Mat2 matrix fib_mat n).
proof: Proof. simple induction n. intro; absurd (0 < 0); auto with arith. intros. rewrite fib_n; unfold M11 in |- *; auto with arith. Qed.
imports: monoid Arith Compare_dec fmpc