proposition: Lemma Exercise1_2f1 r r' f: increasing_fun f r r' -> Ex1_2_hC' r (equivalence_associated f).
proof: Proof. move => [or or' [ff sr sr'] icf]. move=> x y z xy yz. move:(icf _ _ xy)(icf _ _ yz) => sa sb. move/(ea_relatedP ff) => [_ _ sw]; rewrite - sw in sb. apply /(ea_relatedP ff); rewrite sr; split => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)