proposition: Lemma Exercise1_13c E (F := fixpoints f) : complete_lattice r -> sub E F -> inc (infimum r E) F.
proof: Proof. move: cf=> [icf c2 c3] [_ lr] EF. move: (icf) => [or or' [ff sf tf] incf]. have sF: (sub F (substrate r)) by rewrite - sf; apply: Zo_S. have sE: (sub E (substrate r)) by apply: (sub_trans EF). move: (lr _ sE) => [_ hi]; move: (infimum_pr1 or hi). set (y:= infimum r E); move /(glbP or sE)=> [[yE ylb] yglb]. have wy: (inc (Vf f y) (substrate r)) by rewrite - tf; Wtac. apply: Zo_i; first (by ue); apply: (order_antisymmetry or); last by apply: c2. apply: yglb; split => //; move=> u uE; move: (incf _ _ (ylb _ uE)). by move: (EF _ uE) => /Zo_hi ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)