fact: Definition fib_with_chain c := match chain_apply c Mul2 (1,0) with Some ((a,b), nil) => Some (a+b) | _ => None end.
imports: Coq(NArith Ring) additions(Monoid_instances Euclidean_Chains Pow Strategies Dichotomy BinaryStrat) additions(AM)