proposition: Lemma fib_mul2_OK n : fib n = fib_mul2 n.
proof: Proof. unfold fib_mul2; pattern n;apply fib_ind; try reflexivity. - intros; rewrite fib_mul2_OK_0; now rewrite fib_SSn, N.add_comm. Qed.
imports: Coq(NArith Ring) additions(Monoid_instances Euclidean_Chains Pow Strategies Dichotomy BinaryStrat)