proposition: Lemma olim_exten f g x l: esame_below f g x -> (olimit f x l <-> olimit g x l).
proof: Proof. move => [b lbx bp]; split. move =>[[y ya yb] yc]; split. move: (omax_p1 (proj31_1 ya) (proj31_1 lbx)) =>[la lb]. have lc: omax y b <o x by rewrite /omax/Gmax; Ytac h. exists (omax y b) => // i ia ib; move: (oleT la ia)(oleT lb ia) => qa qb. by rewrite - bp //; apply: yb. move => m lm; move: (yc _ lm) => [z za zb]. move: (omax_p1 (proj31_1 za) (proj31_1 lbx)) =>[la lb]. have lc: omax z b <o x by rewrite /omax/Gmax; Ytac h. exists (omax z b) => // i ia ib; move: (oleT la ia)(oleT lb ia) => qa qb. by rewrite - bp //; apply: zb. move =>[[y ya yb] yc]; split. move: (omax_p1 (proj31_1 ya) (proj31_1 lbx)) =>[la lb]. have lc: omax y b <o x by rewrite /omax/Gmax; Ytac h. exists (omax y b) => // i ia ib; move: (oleT la ia)(oleT lb ia) => qa qb. by rewrite bp //; apply: yb. move => m lm; move: (yc _ lm) => [z za zb]. move: (omax_p1 (proj31_1 za) (proj31_1 lbx)) =>[la lb]. have lc: omax z b <o x by rewrite /omax/Gmax; Ytac h. exists (omax z b) => // i ia ib; move: (oleT la ia)(oleT lb ia) => qa qb. by rewrite bp //; apply: zb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)