proposition: Lemma limit12b1 x: (limit12_hyp zero zero x) -> limit_of (phi3 x) [zero, zero, x].
proof: Proof. case x => // [a1 b1 c1 n1 d1] /=. rewrite !T3lt0n /= andbT => /andP[/andP [/eqP -> /eqP ->]]. have ->: (zero == a1) && (b1 != zero) || (a1 != zero) = (a1 != zero) || (b1 != zero). by rewrite eq_sym; case:eqP => //=; rewrite orbF. move => sa; clear n1 d1. split. by apply: fincP => n; rewrite !phi3v T3lt_consE !T3ltnn eqxx ltnS leqnn. by move => n; rewrite phi3v T3lt_consE T3lt_psi_c. case => //; first by move => _ h; exists 0. move => a b c n d /and5P[_ _ nc _ _]; rewrite -/T3nf in nc. rewrite psi_lt1 T3lt_psi' !T3ltn0 !T3lt0n !andbF /= => h. exists (n.+1); rewrite phi3v T3le_consE ltnS leqnn if_simpl -/(orb _ _) orbC. case/orP:h; last by rewrite andbA;case /orP => /andP [_]. move => /and3P[/eqP -> /eqP -> cc]; rewrite /T3le T3lt_psi' cc !T3lt0n. move: sa; case a1z: (a1==zero); rewrite ?orbT //= (eq_sym _ a1) a1z. by move => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)