proposition: Lemma limit12a f a b c: ~~ (limit12_hyp a b c) -> (limit_of f c) -> (limit_of (phi12a a b f)[a, b, c]).
proof: Proof. move => H [sa sb sc]. have gi:forall n m : nat, (n < m)%N -> (phi12a a b f) n < (phi12a a b f) m. by move => n m /sa ha; rewrite T3lt_psi /lt_psi !eqxx ha. split => //. by move => n; rewrite T3lt_psi /lt_psi !eqxx (sb n). move => y. move:{2} (size y).+1 (leqnn (size y).+1) => n; elim: n y=> //. move => m Hrec y; rewrite ltnS. rename a into a1;rename b into b1; rename c into c1. case: y => //; first by move => _ _ _; exists 0; rewrite T3le0n. case: c1 H sb sc Hrec. by move => _ H; move: (H 0); rewrite T3ltn0. move => a2 b2 c2 n2 d2 /=. rewrite !negb_and negb_or !negb_and - !T3leNgt; set c1 := cons _ _ _ _ _. move => H sb sc Hrec a b c n d lm ny; rewrite psi_lt1. have /and5P [_ lb lc _ _]:= (size_prop1 a b c n d). have/and5P [na nb nc nd ne] := ny. have nabc: T3nf [a,b,c] by rewrite nf_psi na nb nc. rewrite T3lt_psi /lt_psi. case /orP. move => /and3P[ha hb hc]. have [k kp] := (sc c nc hc). have ck1 := (T3le_lt_trans kp (sa _ _ (ltnSn k))). by exists k.+1; rewrite T3le_consE T3lt_psi /lt_psi ha hb ck1. case /orP. move => /and3P [ha hb hc]. have [k kp] := (Hrec _ (leq_trans lc lm) nc hc). have ck1 := (T3le_lt_trans kp (gi _ _ (ltnSn k))). by exists k.+1; rewrite T3le_consE T3lt_psi /lt_psi ha hb ck1 !orbT. case /orP. move => /and3P [ha hb hc]. have [k kp] := (sc _ nabc hc). have ck1 := (T3le_lt_trans kp (sa _ _ (ltnSn k))). by exists k.+1; rewrite T3le_consE T3lt_psi /lt_psi ha hb ck1 !orbT. case /orP. move => /and3P [ha hb/eqP hc]. by move: H; case: hc => <- <- cc <- <- /=; rewrite T3leNgt eq_sym ha hb. case /orP. move => /and3P [ha hb hc]. have [k1 k1p] := (Hrec _ (leq_trans lb lm) nb hb). have [k2 k2p] := (Hrec _ (leq_trans lc lm) nc hc). set k := (k1+k2).+1. have hd: b < (phi12a a1 b1 f) k. by apply /(T3le_lt_trans k1p) /gi; rewrite ltnS leq_addr. have he: c < (phi12a a1 b1 f) k. by apply /(T3le_lt_trans k2p) /gi; rewrite ltnS leq_addl. by exists k; rewrite T3le_consE T3lt_psi /lt_psi ha hd he !orbT. case /orP. move => /andP [ha hb]; exists 1. by rewrite T3le_consE T3lt_psi /lt_psi ha (T3lt_ne' ha) (T3lt_anti ha) hb. case /orP. move => /andP [ha hb]; exists 1. by rewrite T3le_consE T3lt_psi /lt_psi ha hb !orbT. case /orP. move => /andP [ha hc]. have [k kp] := (sc _ nabc hc). have ck1 := (T3le_lt_trans kp (sa _ _ (ltnSn k))). by exists k.+1; rewrite T3le_consE T3lt_psi /lt_psi ha ck1 !orbT. move => /andP [ha /eqP hc]; exists 1. rewrite T3le_consE T3lt_psi /lt_psi ha (T3lt_ne' ha) (T3lt_anti ha) hc. move: H; case: (hc) => <- <- cc <- <- /=. by rewrite (T3leNgt a) ha (T3lt_ne ha) /=;case /orP => -> //; rewrite orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)