proposition: Lemma Fib_div n m: n %|c m -> Fib n %|c Fib m.
proof: Proof. move => h;rewrite(cdivides_pr h). move:h => [mN nN _]; move:(NS_quo n mN); set k := (m %/c n). case: (equal_or_not n \0c) => nz. rewrite nz cprod0l Fib0 => _; apply: (cdivides_zero NS0). move:(cpred_pr nN nz) => [sN sv]. move:(k); apply: {m mN k} Nat_induction. rewrite cprod0r Fib0; exact (cdivides_zero (NS_Fib nN)). move => m mN Hrec. have ha:= (cdivides_trans2 (NS_Fib sN) Hrec). have hb: Fib n %|c (Fib (csucc (n *c m)) *c Fib n). rewrite cprodC;apply:cdivides_pr1; apply:NS_Fib; fprops. rewrite (cprod_nS _ mN) {3}sv (csum_nS _ sN) (Fib_add (NS_prod nN mN) sN) - sv. exact (proj1 (cdivides_sum ha hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)