proposition: Lemma ex4_propb a b c x y z: gle r a c -> gle r b c -> inc z (ex4_setEi c) -> x = Vf (ex4_function_f (J a c)) z -> y = Vf (ex4_function_f (J b c)) z -> domain x = domain y -> ex4_fct_s x = ex4_fct_s y.
proof: Proof. move => leac lebc zf. move: (ex4_function_f_ax leac) (ex4_function_f_ax lebc) => ax1 ax2. rewrite /ex4_function_f; aw; rewrite !LfV// => -> ->. rewrite /ex4_function_fv /ex4_modify_r 2!Lgd 2!restr_d. set m := csucc (ex4_indexj z a) => mv; rewrite - mv. rewrite /ex4_fct_s /ex4_last 2!Lgd restr_d. move/Zo_P:(zf) => [zE zr]; rewrite - zr in leac. move:(proj31 (ex4_indexj_correct zE leac)) => lab. move/ex4_inF_hi: zE => [_ [ dN _ _ _ _] _]. have iN:= NS_lt_nat lab dN. have ha: inc (cpred m) m. rewrite (cpred_pr2 iN); apply/(NltP (NS_succ iN))/(cltS iN). by rewrite ! LgV //; Ytac0;Ytac0; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)