proposition: Lemma lens_sinterval (G : graph2) : connected [set: skeleton G] -> lens G -> (@sinterval G input output = ~: IO).
proof: Proof. move=> G_conn /and3P[] /edgeless_bag/eqP-/(_ G_conn (CP_extensive _)). rewrite !inE -setTD eqxx =>/(_ isT) bag_i. move=> /edgeless_bag/eqP-/(_ G_conn (CP_extensive _)). rewrite !inE eqxx orbT =>/(_ isT) bag_o /andP[iNo _]. rewrite (sinterval_bag_cover G_conn iNo) bag_i bag_o setUAC. rewrite setDUl setDv set0U setDE. apply: esym; apply/setIidPl. apply/subsetP=> x x_sI. rewrite !inE negb_or. apply/andP; split; apply: contraTneq x_sI =>->; by rewrite sinterval_bounds. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)