proposition: Lemma Fib_smonotone n m: natp n -> natp m -> n <> \0c -> n <> \1c -> n <c m -> Fib n <c Fib m.
proof: Proof. move => nN mN nz no. case: (equal_or_not m \0c) => mz; first by rewrite mz; move/clt0. move:(cpred_pr mN mz) => [sa ->]; move/(cltSleP sa). move: (cpred m) sa; clear m mN mz; apply:Nat_induction. move => /cle0 ->;rewrite succ_zero Fib0 Fib1; apply: clt_01. move => m mN Hrec; rewrite (Fib_rec mN) csumC. case: (equal_or_not n (csucc m)) => eq1 h. rewrite - eq1; apply: (csum_M0lt (NS_Fib nN)); apply:(Fib_gt0 mN) => mz. by case: no; rewrite eq1 mz succ_zero. move: (Nsum_M0le (Fib m) (NS_Fib (NS_succ mN))). by apply:clt_leT; apply: Hrec; apply /(cltSleP mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)