proposition: Lemma Exercise4_8g: order_on E48Js (irreds r) /\ order_on E48Ps E48P.
proof: Proof. have s1: sub (irreds r) (substrate r) by apply: Zo_S. by move: (Exercise4_8f s1) (Exercise4_8f Exercise4_7e) => [p1 p2][p3 p4]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)