proposition: Theorem dvdn_fib: forall m n, m %| n -> fib m %| fib n.
proof: Proof. move=> m n; 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(all_ssreflect all_algebra)