proposition: Lemma fib_eq : forall m n, (fib m == fib n) = [|| m == n, (m == 1) && (n == 2) | (m == 2) && (n == 1)].
proof: Proof. move=> m n; 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 move: (fib_gt0 _ Hm); rewrite orbF [0 == _]eq_sym !eqn0Ngt Hm; case: (fib n). - by rewrite eq_sym fib_eq1 orbF [1==_]eq_sym; case: eqP. have: 1 < m.+2 < n by []. move/fib_smonotone; rewrite ltn_neqAle; case/andP; move/negPf=> -> _. case: n Hm=> [|[|n]] //;rewrite ltn_neqAle; case/andP; move/negPf=> ->. by rewrite andbF. Qed.
imports: mathcomp(all_ssreflect all_algebra)