proposition: Lemma Int_repr_eq_small: forall a b, 0 <= a < Int.modulus -> 0 <= b < Int.modulus -> Int.repr a = Int.repr b -> a = b.
proof: Proof. intros. apply Int_eqm_unsigned_repr', Int_eqm_unsigned_spec in H1. rewrite Int.unsigned_repr_eq in H1. rewrite Z.mod_small in H1; trivial. pose proof (Int.eqm_small_eq _ _ H1 H H0); trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure