proposition: Lemma Exercise1_7e r r': order r -> order r' -> (exists u v, [/\ inc u (substrate r'), inc v (substrate r') & u <>v]) -> (exists2 x, inc x (substrate r) & cr_component r x <> substrate r) -> exists f, [/\ increasing_fun f r r', decreasing_fun f r r' & ~(constantfp f)].
proof: Proof. move=> or or' [u [v [usr' vsr' uv]]] [x xsr nsr]. move: (cr_properties or)=> [p1 p2 p3 p4 p5]. pose f t := Yo (inc t (cr_component r x)) u v. have ta: (lf_axiom f (substrate r) (substrate r')). by move=> t tsr; rewrite /f; Ytac tc. set (g:= Lf f (substrate r) (substrate r')). have fg: (function g) by apply: lf_function. have sg: source g = substrate r by rewrite /g; aw. have tg: target g = substrate r' by rewrite /g; aw. have q1:(sub (cr_component r x) (substrate r)). by rewrite -(p4 _ xsr) -p3; apply: sub_class_substrate. have q2: forall y, inc y (cr_component r x) -> Vf g y = u. by move=> y yc; rewrite /g LfV // /f; [ Ytac0 | apply: q1]. have q3 y: inc y (substrate r) -> ~(inc y (cr_component r x)) -> Vf g y = v. by move=> yc ync; rewrite /g LfV // /f Y_false //. have ncg: (~ constantfp g). move=> [h1 h2]; case: nsr; apply: extensionality => //. move=> t tsr; ex_middle bad; rewrite sg in h2. have xc: inc x (cr_component r x). rewrite -(p4 _ xsr); apply /(class_P p1); apply: reflexivity_e =>//; ue. case: uv;move: (h2 _ _ xsr tsr);rewrite (q2 _ xc)(q3 _ tsr bad) //. have q4: (forall a b, gle r a b -> ((inc a (cr_component r x) <-> inc b (cr_component r x)))). move=> a b ab; rewrite - (p4 _ xsr). have cab: (ocomparable r a b) by left. move: (p5 _ _ cab)=> rab. split; move => /(class_P p1) => h; apply /(class_P p1). by apply: (@transitivity_e _ a). by apply: (@transitivity_e _ b) =>//; apply: symmetricity_e. have q5: (forall a b, gle r a b -> Vf g a = Vf g b). move=> a b ab. case: (p_or_not_p (inc a (cr_component r x))) => H. by rewrite (q2 _ H); move: H;move/ (q4 _ _ ab) => H; rewrite (q2 _ H). have asr: inc a (substrate r) by order_tac. have bsr: inc b (substrate r) by order_tac. by rewrite (q3 _ asr H); move:H => /(q4 _ _ ab) H;rewrite (q3 _ bsr H). exists g;split => //; split => //; move=> a b ab;rewrite (q5 _ _ ab); order_tac. rewrite -tg; apply: Vf_target => //; rewrite sg; order_tac. rewrite -tg; apply: Vf_target => //; rewrite sg; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)