proposition: Lemma fibonacci : forall n : nat, {q : Z | q = Z_of_nat (Fib n)}.
proof: Proof. refine (fun n => match zerop n with | left e => exist _ 1%Z _ | right l => match addchains dic n Mat2 matrix fib_mat with | exist m e => exist _ (M11 m) _ end end). rewrite e; rewrite Unfold_FibO; auto with arith. rewrite fib_computation. rewrite e; auto with arith. auto with arith. Qed.
imports: Constants generation monoid machine strategies spec log2_spec log2_implementation Compare_dec while imperative develop dicho_strat binary_strat trivial standard monofun matrix ZArith