proposition: Lemma next_fib (n:nat) : mul2 (1,0) (fib (S n), fib n) = (fib (S (S n)), fib (S n)).
proof: Proof. unfold mul2; f_equal; ring_simplify. - rewrite fib_SSn. ring. - reflexivity. Qed.
imports: Coq(NArith Ring) additions(Monoid_instances Euclidean_Chains Pow Strategies Dichotomy BinaryStrat)