proposition: Lemma fib_eq m n: (fib m == fib n) = [|| m == n, (m == 1) && (n == 2) | (m == 2) && (n == 1)].
proof: Proof. wlog: m n/ m <= n=> [HH|]. case/orP: (leq_total m n)=> Hm; first by exact: HH. by rewrite eq_sym HH // eq_sym ![(_ == 1) && _]andbC [(_ && _) || _] orbC. rewrite leq_eqVlt; case/orP; first by move/eqP->; rewrite !eqxx. case: m=> [|[|m]] Hm. - by rewrite (ltn_eqF (fib_gt0 Hm)) (ltn_eqF Hm). - by rewrite eq_sym fib_eq1 orbF eq_sym. have: 1 < m.+2 < n by []. move/fib_smonotone =>/ltn_eqF ->. by case: n Hm=> [|[|n]] // /ltn_eqF -> //; rewrite andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)