proposition: Lemma Exercise1_2f2 r r' f: increasing_fun f r r' -> (weak_order_compatibility r (equivalence_associated f) <-> (Ex1_2_hD r f)).
proof: Proof. move => [or or' [ff sr sr'] icf]. split. move=> [[pr ea sea] ch] x y x' xy x'sf sW. have aux: (related (equivalence_associated f) x x'). apply /ea_relatedP => //; split => //; rewrite sr; order_tac. move: (ch _ _ _ xy aux) => [y' /(ea_relatedP ff) [pa pb pc] x'y']. by exists y'. have [ee se]:=(graph_ea_equivalence ff). move=> ch; split; first split. + by apply: order_preorder. + done. + by rewrite se. + move=> x y y' xy /(ea_relatedP ff) [xsf ysf sv]. move: (ch _ _ _ xy ysf sv) => [z [zf y'z sv1]]. exists z=> //; apply /(ea_relatedP ff);split => //; rewrite sr; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)