proposition: Lemma fib_SSn : forall (n:nat) , fib (S (S n)) = (fib n + fib (S n)).
proof: Proof. intro n; pattern n; apply fib_ind; try reflexivity. Qed.
imports: Coq(NArith Ring) additions(Monoid_instances Euclidean_Chains Pow Strategies Dichotomy BinaryStrat)