proposition: Lemma Exercise1_7d r r' f: increasing_fun f r r' -> decreasing_fun f r r' -> (exists2 x, inc x (substrate r) & cr_component r x = substrate r) -> (constantfp f).
proof: Proof. move=> incf decf [x xsr sr1]; set H := (Exercise1_7c incf decf). move: (incf) => [or or' [ff sr sr'] incf']. move: (cr_properties or)=> [p1 p2 p3 p4 p5]. split => //. suff sw': (forall u, inc u (source f) -> Vf f u = Vf f x). by move => a b asf bsf; move: (sw' _ asf) (sw' _ bsf) => -> ->. move => u; rewrite sr - sr1 -(p4 _ xsr) => /(class_P p1) rxu. have: related (cr_equiv r) u x by apply: symmetricity_e. move /Zo_P => [_]; aw; move => [c [h1 <- <-]]. elim: c h1;first by move => a b; apply: H. by move=> a c => xx [yy zz]; rewrite -(xx zz); apply:H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)