proposition: Lemma inf_A_alt r f c x: order r -> fgraph f -> sub (range f) (substrate r) -> (domain f) = (unionb c) -> (forall l, inc l (domain c) -> has_inf_graph r (restr f (Vg c l))) -> (inf_graphp r f x <-> inf_graphp r (Lg (domain c) (fun l => inf_graph r (restr f (Vg c l)))) x).
proof: Proof. move => ha hb hc he hf. move:(opp_osr ha) =>[or' sr']. move: (hc);rewrite - sr' => hc'. set r':= opp_order r. have pa i: inc i (domain c) -> sub (range (restr f (Vg c i))) (substrate r). move => zc. have pb:sub (Vg c i) (domain f) by rewrite he => t ta; union_tac. by move: (sub_trans (restr_range1 hb pb) hc'); rewrite sr'. have hf' i: inc i (domain c) -> has_sup_graph r' (restr f (Vg c i)). move => lc; move:(hf _ lc); rewrite /has_inf_graph /has_sup_graph => ww. exact (proj1 (inf_sup_opp ha (pa _ lc) ww)). have pc: inf_graphp r f x <-> sup_graphp (opp_order r) f x by apply:inf_sup_oppP. apply: (iff_trans pc); apply: (iff_trans (sup_A or' hb hc' he x hf')). rewrite /sup_graphp /inf_graphp. set a := Lg (domain c) _; set b := Lg (domain c) _. have ->: a = b. apply: Lg_exten => i idc. exact: (proj2 (inf_sup_opp ha (pa _ idc) (hf _ idc))). apply:iff_sym; apply:inf_sup_oppP => //. rewrite /b /inf_graph Lg_range => t /funI_P [z za ->]. apply:(inc_infimum_substrate ha (pa _ za) (hf _ za)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)