proposition: Lemma Exercise1_13d x y: lattice r -> inc x (substrate r) -> inc y (substrate r) -> Vf f (sup r x y) = Vf f (sup r (Vf f x) (Vf f y)).
proof: Proof. move: cf => [icf c1 c2] lr xsr ysr. move: (icf) => [or or' [ff sf tf] incf]. move: (icf); rewrite Exercise1_10b // => aux; move: (aux _ _ xsr ysr). have wxs: inc (Vf f x) (substrate r) by rewrite - tf; Wtac. have wys: inc (Vf f y) (substrate r) by rewrite - tf; Wtac. move: (lattice_sup_pr lr wxs wys) => [p1 p2 _]. move: (order_transitivity or (c1 _ xsr) p1) => p3. move: (order_transitivity or (c1 _ ysr) p2) => p4. move: (lattice_sup_pr lr xsr ysr) => [_ _ aux2]. move: (aux2 _ p3 p4). set z := sup r x y; set T:= (sup r (Vf f x) (Vf f y)). move => p5 p6; move: (incf _ _ p5) (incf _ _ p6); rewrite c2; last order_tac. move=> p7 p8; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)