proposition: Lemma mid_nil : forall (s : seq R), (mid s == [::]) = ((s == [:: s`_0 ; s`_1]) || (s == [:: s`_0]) || (s == [::])).
proof: Proof. case=> [| a [| b]] //=. by rewrite /mid /= orbF !eqxx orbT. case=> [ |c l] //=. by rewrite /mid /= orbF !eqxx orTb. by rewrite /mid /= orbF -eqseqE /= !andbF orbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)