proposition: Lemma Exercise1_10b f: function_prop f (substrate r)(substrate r') -> ((increasing_fun f r r') <-> (forall x y, inc x (substrate r) -> inc y (substrate r) -> gle r' (sup r' (Vf f x) (Vf f y)) (Vf f (sup r x y)))).
proof: Proof. move => [ff sf tf]; split. move=> [or or' _ incf] x y xsr ysr. move: (lattice_sup_pr lr xsr ysr) => [Ha Hb _ ]. have p1: (inc (sup r x y) (source f)) by rewrite sf; order_tac. rewrite - sf in xsr ysr; move: (incf _ _ Ha) (incf _ _ Hb) => p2 p3. move: (Vf_target ff xsr)(Vf_target ff ysr); rewrite tf => w1 w2. by apply: (proj33(lattice_sup_pr lr' w1 w2)). move: (lr)(lr') => [or _][or' _] p;split => //. move=> x y xy. move:(arg1_sr xy)(arg2_sr xy); rewrite - sf => xsr ysr. rewrite - sf in p;move: (p _ _ xsr ysr); rewrite (sup_comparable1 or xy). move: (Vf_target ff xsr)(Vf_target ff ysr); rewrite tf => w1 w2. move: (lattice_sup_pr lr' w1 w2) => [p1 _ _] p2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)