proposition: Theorem dvdn_fib m n: m %| n -> fib m %| fib n.
proof: Proof. case/dvdnP=> n1 ->. elim: {n}n1 m=> [|m IH] // [|n]; first by rewrite muln0. by rewrite mulSn fib_add // dvdn_add //; [apply dvdn_mull | apply dvdn_mulr]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)