proposition: Lemma Exercise4_8iP K (o := opp_order (induced_order r K)) (A:= increasing_mappings o E48Io): sub K (substrate r) -> forall f, inc f A <-> [/\ function f, source f = K, target f = E48I & (forall i j, inc i K -> inc j K -> gle r i j -> Vf f j = \1c -> Vf f i = \1c)].
proof: Proof. move=> Ksr f. move: Exercise4_8h (Exercise4_8f Ksr) => [o1 s1] [o2 s2]. have oi: order r by move: lr => [or _]. move: (iorder_osr oi Ksr) => [o0 s0]. split. move /soimP => [[ff sf tf] incf]; split => //; try ue. move => i j isr jsr ij f1. move:incf => [p1 p2 [p3 p4 p5] p6]. have aux: gle o j i by apply /opp_gleP/iorder_gleP;split => //. move: (p6 _ _ aux); rewrite f1;move /Ninto_gleP => [_] /(NintcP NS1). apply: cleA. move=> [ff sf tf incf]. have aux: function_prop f (substrate o) (substrate E48Io) by split => //; ue. apply /soimP; split => //; split => //. move => x y / opp_gleP /iorder_gleP [xk yk yx]. have wx: inc (Vf f x) (target f) by Wtac. have wy: inc (Vf f y) (target f) by Wtac. move: s1; rewrite (proj2 (Ninto_wor \0c \1c)) => ww. rewrite tf in wx wy;apply /(Ninto_gleP); rewrite ww;split => //. move: (incf _ _ xk yk yx). case /set2_P: wx => -> ; case /set2_P: wy => ->; fprops => h; try apply:cle_01. by move: (h (erefl \1c)) => ->; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)