proposition: Lemma div_pos_le: forall a b, 0 <= a -> 0 < b -> a / b <= a.
proof: Proof. intros. rewrite <- (Z2Nat.id a); trivial. rewrite <- (Z2Nat.id b); [|lia]. remember (Z.to_nat a) as n1. remember (Z.to_nat b) as n2. rewrite <- div_Zdiv by lia. apply inj_le. replace n1 with (Nat.div n1 1) at 2. 2: apply Nat.div_1_r. apply Nat.div_le_compat_l. lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph