proposition: Lemma Int_signed_strip: forall a b, Int.signed a = Int.signed b -> a = b.
proof: Proof. intros. pose proof (Int.signed_eq a b). unfold zeq in H0. destruct (Z.eq_dec (Int.signed a) (Int.signed b)). simpl in H0. apply int_eq_e; trivial. exfalso. apply n. trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure