proposition: Lemma fooCE (x:= T1bad): ~~T1limit x /\(forall u v, T1limit u -> x <> u + \F v.+1).
proof: Proof. by split => // u v; case u => // a n b; case a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)