proposition: Lemma Fib_monotone n m: natp n -> natp m -> n <=c m -> Fib n <=c Fib m.
proof: Proof. move => nN mN le; move:(CS_nat (NS_Fib mN)) => h. case:(equal_or_not n m) => eq; first by rewrite eq; apply: (cleR h). case:(equal_or_not n \0c) => eq2; first by rewrite eq2 Fib0; apply: cle0x. case:(equal_or_not n \1c) => eq3. move: le; rewrite eq3 Fib1 => hh; apply:(cge1 h); apply:(Fib_gt0 mN) => mz. apply: (cleNgt hh); rewrite mz; fprops. exact (proj1(Fib_smonotone nN mN eq2 eq3 (conj le eq))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)