proposition: Lemma limit7 x y f: (limit_of f y) -> (limit_of ( phi7 x y f) [x,y,zero]).
proof: Proof. move => [sa sb sc]. set g := (phi7 x y f). have ff:forall n m : nat, (n < m)%N -> g n < g m. by apply: fincP => n /=; apply: T3lt_psi_c. split => //. elim; first by apply: T3lt_psi_b. by move => n /= H; rewrite /= T3lt_psi /lt_psi H eqxx sb /= !orbT. move => t. move:{2} (size t).+1 (leqnn (size t).+1) => n; elim: n t=> //. move => m Hrec t; rewrite ltnS. case: t => //; first by move => _ _ _; exists 0; rewrite T3le0n. move => a b c n d lm nt; rewrite psi_lt1. move: nt; rewrite /T3nf -/T3nf => /and5P [na nb nc _ _]. move /and5P: (size_prop1 a b c n d) => [la lb lc ld _]. rewrite T3lt_psi' /lt_psi T3ltn0 T3len0 !andbF /=. case /orP. move /and3P => [ax lby cz]. have [k2 kp2] := (sc _ nb lby). have [k1 kp1] := (Hrec _ (leq_trans lc lm) nc cz). set k := (k1 + k2).+1. have pa:(b < f k) by apply/(T3le_lt_trans kp2) /sa; rewrite ltnS leq_addl. have pb: (c < g k.+1) by apply/(T3le_lt_trans kp1) /ff; rewrite /k ltnS -addnS leq_addr. by exists (k.+1); rewrite T3le_consE T3lt_psi/lt_psi ax pa pb !orbT. case /orP. move /and3P => [ax bz cz]. have [k1 kp1] := (Hrec _ (leq_trans lc lm) nc cz). have [k2 kp2] := (Hrec _ (leq_trans lb lm) nb bz). set k := (k1 + k2).+1. have pa:(b < g k) by apply/(T3le_lt_trans kp2) /ff; rewrite ltnS leq_addl. have pb:(c < g k) by apply/(T3le_lt_trans kp1) /ff; rewrite ltnS leq_addr. by exists k; rewrite T3le_consE T3lt_psi/lt_psi ax pa pb !orbT. rewrite orbF => /andP [ha hb]. exists 1. by rewrite T3le_consE T3lt_psi/lt_psi ha; case/orP: hb => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)