proposition: Lemma like_fib_add F F': like_fib F -> like_fib F' -> like_fib (fun n => F n + F' n).
proof: Proof. by move => h1 h2 n; rewrite addnACA - h1 - h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)