proposition: Lemma Exercise1_7c r r' f: increasing_fun f r r' -> decreasing_fun f r r' -> forall x y, ocomparable r x y -> Vf f x = Vf f y.
proof: Proof. move=> [or or' [ff sr sr'] incf][_ _ _ decf] x y. case=> h; move: (decf _ _ h)(incf _ _ h)=> p1 p2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)