proposition: Lemma Exercise4_8m: order_on E48AJImo (E48AJI -s1 E48z) /\ forall f, inc f (substrate E48AJImo) <-> (inc f E48AJI /\ Vf f (the_least r) = \1c).
proof: Proof. move: Exercise4_8k Exercise4_8l => [[p1 p2] _] p3. have p4:sub (E48AJI -s1 E48z) E48AJI by apply: sub_setC. move: p4; rewrite -p2 => p5. have p6:substrate E48AJImo = E48AJI -s1 E48z. rewrite /E48AJImo iorder_sr//; ue. split; first by apply:(iorder_osr p1 p5). move: Exercise4_7d => lj. have ta:lf_axiom (fun _ : Set => \0c) (irreds r) E48I. rewrite /E48I => t _; fprops. rewrite p6 p2=> f; split; last first. move=> [p7 p8];apply /setC1_P; split => //. move=> sf; rewrite sf in p8; move: p8; rewrite /E48z LfV//; fprops. move /setC1_P => [p7 p8];split => //. have s1: sub (irreds r) (substrate r) by apply: Zo_S. move: p7 => /(Exercise4_8iP s1) [ff sf tf icf]. move: (lj); rewrite - sf => lj1. move: (Vf_target ff lj1);rewrite tf; case /set2_P => // wlp. case: p8; rewrite /E48z;apply: function_exten;aw; trivial. by apply: lf_function. move=> x xsf; move: (xsf); rewrite sf => xsr; rewrite LfV //. move: (Vf_target ff xsf);rewrite tf; case /set2_P => // wo. move: lr => [or _]. move: (the_least_pr or Exercise4_7c) => [_ tle]. move: (icf _ _ lj xsr (tle _ (s1 _ xsr)) wo). by rewrite wlp; move=> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)