proposition: Lemma Exercise2_7dP f g: inc f closures -> inc g closures -> (gle (closure_ordering) f g <-> sub (fixpoints g) (fixpoints f)).
proof: Proof. move=> fs gs; move: (fs) => /Zo_P [/functionsP [ff sf tf] [q1 q2 q3]]. move: (gs) => /Zo_P [/functionsP [fg sg tg] [q4 q5 q6]]. split. move /Exercise2_7aP=> [_ _ h] t /Zo_P [tsg wg]; apply /Zo_P;split. by rewrite sf - sg. rewrite sg in tsg; move: (q2 _ tsg) => p11. move: (h _ tsg) ; rewrite wg=> p7; order_tac. move=> h; apply /Exercise2_7aP;split => // i isr. move: (q5 _ isr) (q6 _ isr) => le1 le2. have : inc (Vf g i) (fixpoints f). apply: h; apply: Zo_i=> //; rewrite sg - tg; Wtac; ue. by move /Zo_P=> [_ <-]; move: q1 => [_ _ _ incf]; apply: incf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)