proposition: Lemma like_fib_eq F F': like_fib F -> like_fib F' -> F 0 = F' 0 -> F 1 = F' 1 -> F =1 F'.
proof: Proof. move => ha hb hc hd n. suff: F n = F' n /\ F n.+1 = F' n.+1 by case. by elim:n => // n [he hf]; split => //; rewrite ha hb he hf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)