proposition: Lemma Exercise1_13a x (F := fixpoints f): inc x (source f) -> least (induced_order r (upper_bounds F r x)) (Vf f x).
proof: Proof. move: cf => [icf c1 c2] xsf. move: icf => [or or' [ff sf tf] incf]. have wfl: (inc (Vf f x) (upper_bounds F r x)). apply: Zo_i; last by apply: c1; ue. apply: Zo_i; [ by rewrite sf - tf; Wtac | apply: c2; ue]. have ssr: (sub (upper_bounds F r x) (substrate r)). apply: (@sub_trans F) ;[ apply: Zo_S | rewrite - sf;apply: Zo_S]. rewrite /least iorder_sr //; split => //. move=> y ysu; apply /iorder_gle0P => //. move: ysu => /Zo_P [] /Zo_P [ysf Wy] xy; move: (incf _ _ xy); rewrite Wy //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)