proposition: Lemma left_or_right (pg: PreGraph V E) (bi: BinGraph pg left_out_edge right_out_edge): forall x e, vvalid pg x -> evalid pg e -> src pg e = x -> {e = left_out_edge x} + {e = right_out_edge x}.
proof: Proof. intros. pose proof only_two_edges x e. destruct_eq_dec e (left_out_edge x); [left | right]; tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph