proposition: Lemma fooCE (x:= T3bad): ~~T3limit x /\(forall u v, T3limit u -> x <> u + \F v.+1).
proof: Proof. split => // u v; case: u => // a b c n d /=. rewrite all_zeroE T3lt1 T3gt1. by case x1: ([a, b, c] == one) => // h /= xa; move: x1; case: xa=> <- <- <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)