proposition: Lemma like_fib_shiftE F m n: like_fib F -> F (n+m).+1 = F (n.+1)* fib m.+1 + F n * fib m.
proof: Proof. move => ha. by rewrite -addnS addnC (like_fibE(like_fib_shift n ha) m) add0n add1n addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)