proposition: Lemma Exercise1_6q: singletonp E -> total_order r' -> total_order (increasing_mappings_order r r').
proof: Proof. move=> [s sr] [orf torf]. move: (imo_osr r or') => [pa pb]. split => //; rewrite pb=> x y xs ys. move: (xs)(ys) => /soimP [[fx sx tx] ix] /soimP [[fy sy ty] iy]. move: (sx)(sy); rewrite -/E sr=> sx' sy'. have w1:(inc (Vf x s) F) by rewrite /F -tx; Wtac; ue. have w2:(inc (Vf y s) F) by rewrite /F -ty; Wtac; ue. case: (torf _ _ w1 w2) => h; [left | right ]; by apply /imo_gleP => //;split => //; split => // i isr; move: isr; rewrite -/E sr => /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)