proposition: Lemma exclusively_In: forall (a : V) l1 l2, (In a l1 <-> ~ In a l2) <-> (~ In a l1 <-> In a l2).
proof: Proof. intros. destruct (in_dec V_EqDec a l1); destruct (in_dec V_EqDec a l2); split; intros; split; intros; trivial; try contradiction. - apply H in i. contradiction. - apply <- H in i0. contradiction. - apply <- H in n0. contradiction. - apply H in n. contradiction. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph