proposition: Lemma fib_mul2_OK_0 (n:nat) : power (M:=Mul2) (1,0) (S (S n)) = (fib (S n), fib n).
proof: Proof. induction n. - reflexivity. - now rewrite power_eq2, IHn, next_fib. Qed.
imports: Coq(NArith Ring) additions(Monoid_instances Euclidean_Chains Pow Strategies Dichotomy BinaryStrat)