proposition: Lemma Exercise1_6o: nonempty E -> total_order (increasing_mappings_order r r') -> total_order r'.
proof: Proof. move=> [t te] [orf torf]. split => // x y xsr ysr. move: (constant_increasing xsr) (constant_increasing ysr). rewrite (proj2 (imo_osr r or')) in torf. by move => p1 p2; case: (torf _ _ p1 p2) => h; move: (imo_incr or' h te); rewrite !constant_V // => h1 ; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)