proposition: Lemma strict_increasing_extens f g r r': strict_increasing_fun f r r'-> strict_increasing_fun g r r' -> worder r -> Imf f = Imf g -> f = g.
proof: Proof. move=> sif sig wo. have to: total_order r by apply: worder_total. have sm: (strict_monotone_fun f r r') by left. have smg: (strict_monotone_fun g r r') by left. have injf:= (total_order_monotone_injective to sm). have injg:= (total_order_monotone_injective to smg). move:sif sig=> [or or' [ff sr sr'] si] [_ _ [fg srg sr'g] sig] rr {sm smg}. case:(worder_prop2 (fun x=> Vf f x = Vf g x) wo) => H. apply: function_exten=>//; try ue. move: H =>[x [xsr xb sc]]. have xsf: inc x (source f) by ue. have xsg: inc x (source g) by ue. have: inc (Vf f x) (Imf g) by rewrite -rr; Wtac. move/(Imf_P fg) => [y ysg WW]. move:(ysg); rewrite srg - sr=> ysf. have: inc (Vf g x) (Imf f) by rewrite rr; Wtac. move/(Imf_P ff) => [z zsf WWw]. move:(zsf); rewrite sr - srg=> zsg. have ysr: inc y (substrate r) by rewrite srg in ysg. have zsr: inc z (substrate r) by rewrite sr in zsf. have p1: glt r' (Vf g x) (Vf f x). have a0: y <> x by move => h; case: xb; rewrite WW h. rewrite WW; case: (total_order_pr1 to ysr xsr) => // h;last by apply: sig. by move: (sc _ h); rewrite - WW => eq1; case:a0; apply: (proj2 injf). have p2: glt r' (Vf f x) (Vf g x). have a0: x <> z by move => h; case: xb; rewrite WWw h. rewrite WWw; case: (total_order_pr1 to xsr zsr) => h //; first by apply: si. by move: (sc _ h); rewrite - WWw => eq1; case:a0; apply: (proj2 injg). order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)