proposition: Lemma Exercise4_7k a b: gle r a b -> sub (E47S r a) (E47S r b).
proof: Proof. move: Exercise4_7b=> or ab t. move /Zo_P => [p1 [p2 p3]]; apply /Zo_P; split => //; split => //;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)