proposition: Lemma Exercise4_7p: let tg := (irreds r) in order_morphism (Lf (E47S r) (substrate r) (\Po tg)) r (subp_order tg).
proof: Proof. move: lr => [or _] tg. have ta: forall x, inc x (substrate r) -> inc (E47S r x) (\Po tg). by move=> x xsr; apply /setP_P => t /Zo_P [p1 [p2 p3]]; apply /Zo_P. move: (subp_osr tg) => [pa pb]. split; fprops; rewrite ? pb;first by saw; apply: lf_function. hnf; aw;move=> x y xsr ysr; hnf;rewrite !LfV//; split. move => pa1; apply /sub_gleP;split;fprops. by apply: Exercise4_7k. by move /sub_gleP => [pa1 [pb1 pc]]; apply:Exercise4_7m. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)