proposition: Lemma Fib_gt1 n: natp n -> \2c <c n -> \1c <c Fib n.
proof: Proof. move => nN h. by move:(Fib_smonotone NS2 nN card2_nz (nesym card_12) h); rewrite Fib2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)