proposition: Lemma is_fib F: like_fib F -> F 0 = 0 -> F 1 = 1 -> F =1 fib.
proof: Proof. by move => sa sb sc; apply:like_fib_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)