proposition: Lemma Fib_eq n m: natp n -> natp m -> (Fib n = Fib m <-> [\/ n = m, (n = \1c /\ m = \2c) |(n = \2c /\ m = \1c) ]).
proof: Proof. move => nN mN; split; last first. by case; first (by move ->); move => [-> ->]; rewrite Fib1 Fib2. wlog : n m nN mN / n <=c m => H. case: (NleT_ee nN mN); [by apply:H | move => le eq]. case: (H _ _ mN nN le (sym_eq eq)). + by constructor 1. + by move => [sa sb]; constructor 3. + by move => [sa sb]; constructor 2. case: (equal_or_not n m) => enm eq; first by constructor 1. case: (equal_or_not n \0c) => nz. by rewrite nz in enm; move:(Fib_gt0 mN (nesym enm));rewrite - eq nz Fib0;case. case: (equal_or_not n \1c) => n1. case: (equal_or_not \2c m) => m2; first by constructor 2. have: \2c <c m. by split => //; rewrite - succ_one; apply/(cleSltP NS1); rewrite - n1. by move/(Fib_gt1 mN); rewrite - eq n1 Fib1; case. by case: (proj2(Fib_smonotone nN mN nz n1 (conj H enm))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)