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