proposition: Lemma inf_gt_largest_edge: forall (g: DijkGG) e, evalid g e -> elabel g e < inf.
proof: Proof. intros. pose proof (size_representable g). assert (size = 1 \/ size > 1) by lia. destruct H1. * apply size1_bound; trivial. * pose proof (valid_edge_bounds g _ H). pose proof (inf_further_restricted g). apply Z.le_lt_trans with (m := (Int.max_signed / size)). lia. apply Z.le_lt_trans with (m := (Int.max_signed / size) * (size - 1)); trivial. apply Z.le_mul_diag_r; [|lia]. apply Z.div_str_pos; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph